Theorem impd 415

Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)

Hypothesis

Ref	Expression
impd.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
impd	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem impd

Step	Hyp	Ref	Expression
1		impd.1	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	com3l 90	. . 3 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	imp 411	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
4	3	com12 33	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  impcomd  416  imp32  423  imp4b  426  imp4c  428  imp4d  429  imp5d  444  imp5g  446  pm3.31  454  expimpd  458  expl  462  ancomsd  470  syland  614  3expib  1138  ax13lem1  2408  equs5  2494  rsp2  3282  moi  3684  reu6  3692  elpwunsn  4646  opthpr  4812  preqsnd  4820  opthprneg  4826  3elpr2eq  4867  invdisj  5091  snopeqop  5480  solin  5587  sotr2  5594  wefrc  5646  relop  5827  elinxp  6009  reuop  6284  dfpo2  6287  tz7.7  6376  ordtr2  6395  funopsnOLD  7135  tpres  7189  funfvima  7218  isomin  7325  sorpsscmpl  7721  peano5  7878  resf1ext2b  7920  f1oweALT  7957  poxp  8112  soxp  8113  tfr3  8374  tz7.48-1  8418  omordi  8539  odi  8552  omass  8553  oen0  8560  nndi  8597  nnmass  8598  nnmordi  8605  eroveu  8798  ssfi  9145  findcard3  9231  fiint  9274  suplub  9408  hartogs  9494  card2on  9504  unxpwdom2  9538  inf3lem2  9586  ttrclselem2  9683  epfrs  9688  tcel  9700  frr3g  9716  dfac2b  10102  infpssr  10280  isf32lem9  10333  axdc3lem4  10425  axcclem  10429  zorn2lem7  10474  ttukeylem6  10486  brdom6disj  10504  ondomon  10535  inar1  10748  gruen  10785  indpi  10880  nqereu  10902  genpn0  10976  distrlem1pr  10998  distrlem5pr  11000  ltexprlem1  11009  reclem4pr  11023  addsrmo  11046  mulsrmo  11047  supsrlem  11084  lelttr  11288  ltlen  11299  fzind  12685  xrlelttr  13172  xnn0xaddcl  13252  fzen  13560  bernneq  14256  swrdswrdlem  14731  repsdf2  14805  limsupbnd2  15524  mulcn2  15637  prodmolem2  15979  dvdsmod0  16306  lcmfunsnlem1  16685  divgcdcoprm0  16713  maxprmfct  16758  pceu  16896  dvdsprmpweqnn  16935  oddprmdvds  16953  infpnlem1  16960  prmgaplem6  17106  imasaddfnlem  17572  initoeu1  18058  termoeu1  18065  plelttr  18388  gsumval2a  18733  cycsubm  19264  symgfix2  19477  psgnunilem4  19558  lsmmod  19736  efgrelexlemb  19811  imasabl  19937  pgpfac1lem5  20142  rngqiprngimf1lem  21396  rngqiprngimfo  21403  ssdifidlprm  21446  nzerooringczr  21590  lindfrn  21931  mat1dimcrng  22595  dmatelnd  22614  mdetunilem7  22736  cpmatacl  22834  cpmatmcllem  22836  lmss  23416  hausnei2  23471  isnrm2  23476  isnrm3  23477  cmpsublem  23517  2ndcdisj  23574  txcnpi  23726  tx1stc  23768  fgcl  23996  ufileu  24037  fmfnfmlem4  24075  fmfnfm  24076  alexsubALTlem4  24168  alexsubALT  24169  tmdgsum2  24214  prdsxmslem2  24647  ovolicc2  25642  volfiniun  25667  dyadmax  25718  ellimc3  25999  dvlip2  26115  dvne0  26131  dvfsumlem2  26147  taylthlem2  26495  zabsle1  27418  2lgslem3  27526  2sqreulem3  27575  ltlesnd  27897  cutsun12  27941  mulsproplem9  28275  mulsprop  28281  bdayons  28427  n0ssoldg  28504  eucliddivs  28527  bdayfinbndlem1  28618  axcontlem4  29226  uhgr2edg  29467  ushgredgedg  29488  ushgredgedgloop  29490  nb3grprlem1  29639  rusgr1vtx  29847  wlkonl1iedg  29922  uhgrwkspthlem2  30012  usgr2wlkneq  30014  usgr2trlncl  30018  uspgrn2crct  30066  wspthsnonn0vne  30175  usgrwwlks2on  30216  umgrwwlks2on  30217  elwspths2on  30220  elwspths2onw  30221  clwlkclwwlkf1lem3  30266  erclwwlktr  30282  erclwwlkntr  30331  frgrnbnb  30553  frgr2wwlk1  30589  frrusgrord  30601  wlkl0  30627  isch3  31502  ocin  31557  shmodsi  31650  spansneleq  31831  stj  32496  atom1d  32614  atcvat2i  32648  chirredlem1  32651  chirredi  32655  mdsymlem3  32666  mdsymlem6  32669  bnj849  35230  fineqvinfep  35433  pconnconn  35594  cvmsss2  35637  cvmliftlem7  35654  satfv0  35721  satfv0fun  35734  satffunlem  35764  satffunlem1lem1  35765  satffunlem2lem1  35767  mclsind  35933  dfon2lem9  36152  dfon2  36153  cgrextend  36371  btwntriv2  36375  btwncomim  36376  btwnexch3  36383  funtransport  36394  ifscgr  36407  colinearxfr  36438  lineext  36439  fscgr  36443  outsideoftr  36492  trer  36689  finminlem  36691  fnessref  36730  fgmin  36743  axnulregtco  36853  bj-andnotim  37043  bj-alanim  37082  bj-axreprepsep  37572  bj-0int  37603  relowlssretop  37869  finorwe  37888  finxpsuclem  37903  wl-ax13lem1  38000  poimirlem29  38160  itg2addnclem3  38184  itg2addnc  38185  areacirc  38224  ismtybndlem  38317  heibor1lem  38320  iss2  38855  disjlem17  39413  membpartlem19  39425  prtlem17  39512  riotasvd  39592  lshpsmreu  39745  atnle  39953  cvratlem  40057  cvrat2  40065  3dim1  40103  2llnjN  40203  2lplnj  40256  linepsubN  40388  pmapsub  40404  paddasslem14  40469  pclfinN  40536  ispsubcl2N  40583  pclfinclN  40586  ldilval  40749  trlord  41205  cdlemk36  41549  dihlsscpre  41870  baerlem3lem2  42346  baerlem5alem2  42347  baerlem5blem2  42348  pellexlem5  43422  pellex  43424  pell1234qrmulcl  43444  pellfundex  43475  cantnfresb  43913  omabs2  43921  relexpmulnn  44297  clsk1indlem3  44631  19.41rg  45124  iunconnlem2  45508  relpmin  45526  or2expropbi  47626  fcoresf1  47661  euoreqb  47701  2reu8i  47705  dfatcolem  47847  f1oresf1o2  47883  nltle2tri  47905  imasetpreimafvbijlemf1  48008  iccpartnel  48042  ich2exprop  48075  ichreuopeq  48077  paireqne  48115  prprelprb  48121  reupr  48126  reuopreuprim  48130  nprmmul3  48133  fmtnofac2lem  48175  sfprmdvdsmersenne  48210  lighneallem3  48214  lighneallem4  48217  requad2  48243  bgoldbtbnd  48429  dfnbgr6  48477  isubgredg  48486  grimuhgr  48507  grimco  48509  uhgrimedgi  48510  isuspgrimlem  48515  clnbgrgrimlem  48553  grimedg  48555  gpgvtxedg0  48683  gpgvtxedg1  48684  gpgedg2ov  48686  gpgedg2iv  48687  pgnbgreunbgrlem1  48733  pgnbgreunbgrlem2lem1  48734  pgnbgreunbgrlem2lem2  48735  pgnbgreunbgrlem2lem3  48736  pgnbgreunbgrlem2  48737  pgnbgreunbgrlem3  48738  pgnbgreunbgrlem4  48739  pgnbgreunbgrlem5  48743  pgnbgreunbgrlem6  48744  pgnbgreunbgr  48745  upgrwlkupwlk  48760  ldepspr  49104  affinecomb1  49333  itsclc0  49402  aacllem  50430