Theorem imp 115

Description: Importation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)

Hypothesis

Ref	Expression
imp.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
imp	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem imp

Step	Hyp	Ref	Expression
1		simpl 102	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2		simpr 103	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3		imp.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 2, 3	sylc 56	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100

This theorem is referenced by:  impcom  116  impd  242  imp31  243  imp32  244  expdimp  246  impancom  247  pm3.22  252  ancoms  255  adantr  261  biimpa  280  biimpar  281  biimpac  282  biimparc  283  pm3.33  327  pm3.34  328  pm3.35  329  pm5.31  330  imp4b  332  imp41  335  imp42  336  imp43  337  imp44  338  imp45  339  imp5g  342  expr  357  impac  363  sylan9  389  sylan9r  390  imdistani  419  mpan10  443  anabsi5  513  anim12dan  532  pm3.43  534  con3and  564  imnan  624  jaoian  709  jaodan  710  impidc  755  pm2.5dc  763  con2bidc  769  pm5.18dc  777  dfandc  778  pm4.63dc  780  annimim  782  pm4.54dc  805  pm4.79dc  809  orcanai  837  annimdc  845  pm4.55dc  846  pm4.82  857  pm3.11dc  864  pm3.12dc  865  dn1dc  867  3jcad  1085  3expia  1106  3an1rs  1116  3imp1  1117  3imp2  1119  syl3anl2  1184  3jaoian  1200  3jaodan  1201  mp3anl1  1226  mp3anl2  1227  mp3anl3  1228  ecased  1239  xor3dc  1278  pm5.15dc  1280  xor2dc  1281  xornbidc  1282  xordc  1283  nbbndc  1285  biassdc  1286  bilukdc  1287  dfbi3dc  1288  pm5.24dc  1289  xordidc  1290  alanimi  1348  19.29  1511  equs4  1613  equsexd  1617  spimth  1623  equs5a  1675  ax11v2  1701  ax11b  1707  equs5or  1711  sb5rf  1732  equvin  1743  nfsb4t  1890  eu5  1947  mopick  1978  euexex  1985  2euswapdc  1991  exists2  1997  eqrdav  2039  dvelimdc  2197  nebidc  2285  pm13.18  2286  nelne1  2295  nelne2  2296  ralrimdvv  2403  r19.21bi  2407  r19.26  2441  ralbi  2445  rexbi  2446  r19.29  2450  vtoclgft  2604  rspcva  2654  rspc2va  2663  elabgt  2684  eqeu  2711  mob2  2721  mob  2723  euind  2728  reu6  2730  reuind  2744  sbctt  2824  rspsbca  2841  sbcnestgf  2897  rspcsbela  2905  ssel2  2940  sselda  2945  sstr  2953  nssne1  3001  nssne2  3002  reuss2  3217  reupick  3221  reupick2  3223  reximdva0m  3236  ssn0  3259  disjel  3274  ssdisj  3277  disjpss  3278  absneu  3442  preqr1g  3537  prel12  3542  dfiun2g  3689  nbrne1  3781  nbrne2  3782  mpteq12f  3837  triun  3867  csbexga  3885  iinexgm  3908  prexgOLD  3946  prexg  3947  copsex2t  3982  swopo  4043  poirr  4044  potr  4045  pofun  4049  issod  4056  ordelss  4116  trssord  4117  limelon  4136  trsuc  4159  eusvnfb  4186  rabxfrd  4201  regexmidlem1  4258  nordeq  4268  suc11g  4281  nnsuc  4338  brrelex12  4381  vtoclr  4388  optocl  4416  relop  4486  brcogw  4504  breldmg  4541  elreldm  4560  riinint  4593  issref  4707  xpidtr  4715  trin2  4716  cnveqb  4776  funopg  4934  funssres  4942  fununi  4967  funimass2  4977  imain  4981  fnun  5005  fco  5056  opelf  5062  f1oun  5146  fun11iun  5147  fv3  5197  ndmfvg  5204  fvelima  5225  fvopab3ig  5246  fvmptssdm  5255  fvmptf  5263  fvimacnv  5282  fmptco  5330  funfvima2  5391  funfvima3  5392  f1veqaeq  5408  f1ocnvfvrneq  5422  fliftfun  5436  isotr  5456  isoini  5457  isopolem  5461  isosolem  5463  moriotass  5496  acexmidlem2  5509  suppssfv  5708  suppssov1  5709  f1dmex  5743  releldm2  5811  f1o2ndf1  5849  poxp  5853  tposf2  5883  iunon  5899  smoel2  5918  tfrlem9  5935  tfrexlem  5948  tfri3  5953  sucinc2  6026  nnacom  6063  nnmcom  6068  nnsucsssuc  6071  nntri2or2  6076  nnaordi  6081  nnmordi  6089  nnaordex  6100  nnm00  6102  ectocld  6172  iinerm  6178  th3qlem2  6209  f1oen3g  6234  f1oeng  6237  en2d  6248  en3d  6249  dom2lem  6252  fundmen  6286  fundmeng  6287  unen  6293  xpdom2  6305  xpdom2g  6306  fopwdom  6310  nneneq  6320  phpm  6327  phpelm  6328  fin0  6342  findcard  6345  diffifi  6351  ac6sfi  6352  onunsnss  6355  ordiso2  6357  carden2bex  6369  ltmpig  6437  enq0sym  6530  addnq0mo  6545  mulnq0mo  6546  prarloclem3step  6594  prarloclem3  6595  genpml  6615  genpmu  6616  genprndl  6619  genprndu  6620  genpdisj  6621  distrlem1prl  6680  distrlem1pru  6681  distrlem4prl  6682  distrlem4pru  6683  distrlem5prl  6684  distrlem5pru  6685  ltsopr  6694  ltaddpr  6695  addcanprleml  6712  addcanprlemu  6713  recexprlemm  6722  recexprlemlol  6724  recexprlemupu  6726  aptiprleml  6737  aptiprlemu  6738  caucvgprlemnkj  6764  caucvgprlemnbj  6765  addsrmo  6828  mulsrmo  6829  srpospr  6867  caucvgsr  6886  axprecex  6954  mulgt0  7093  ltne  7103  cnegexlem1  7186  cnegexlem2  7187  addgt0  7443  addgegt0  7444  addgtge0  7445  addge0  7446  recexre  7569  mulge0  7610  recexap  7634  prodgt02  7819  prodge02  7821  ltmul12a  7826  mulgt1  7829  nndivtr  7955  addltmul  8161  elnnnn0b  8226  elnnz  8255  zmulcl  8297  nn0n0n1ge2  8311  nn0lt2  8322  uzind2  8350  nn0ind-raph  8355  eluzp1m1  8496  uz3m2nn  8515  negm  8550  lbzbi  8551  qaddcl  8570  qmulcl  8572  qreccl  8576  ledivge1le  8652  xrltne  8729  xrre  8733  xrre2  8734  xrre3  8735  ge0gtmnf  8736  xltnegi  8748  iccsupr  8835  icoshft  8858  icoshftf1o  8859  fznlem  8905  fzen  8907  uzsubsubfz  8911  fzsuc2  8941  elfz1b  8952  elfz0ubfz0  8982  elfz0fzfz0  8983  fz0fzelfz0  8984  fz0fzdiffz0  8987  elfzmlbmOLD  8989  elfzmlbp  8990  difelfznle  8993  fzofzim  9044  eluzgtdifelfzo  9053  elfzodifsumelfzo  9057  elfzonlteqm1  9066  elfzom1p1elfzo  9070  ssfzo12bi  9081  subfzo0  9097  frec2uzlt2d  9190  frecuzrdgfn  9198  iseqid3  9245  m1expcl2  9277  expge1  9292  leexp2r  9308  expubnd  9311  zesq  9367  expnlbnd  9373  rexanuz  9587  rexuz3  9588  r19.29uz  9590  r19.2uz  9591  absnid  9671  leabs  9672  ltabs  9683  icodiamlt  9776  climcn2  9830  climcau  9866  climcaucn  9870  ialgfx  9891  bj-prexg  10031  peano5set  10064  peano5setOLD  10065  bj-peano4  10080  bj-nn0suc  10089  bj-nn0sucALT  10103  bj-findis  10104