Theorem impd 416

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 412	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
4	3	com12 33	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  impcomd  417  imp32  424  imp4b  427  imp4c  429  imp4d  430  imp5d  445  imp5g  447  pm3.31  455  expimpd  459  expl  463  ancomsd  471  syland  615  3expib  1140  ax13lem1  2404  equs5  2490  rsp2  3280  moi  3676  reu6  3684  elpwunsn  4645  opthpr  4811  preqsnd  4819  opthprneg  4825  3elpr2eq  4866  invdisj  5089  snopeqop  5478  solin  5586  sotr2  5593  wefrc  5645  relop  5828  elinxp  6010  reuop  6289  dfpo2  6292  tz7.7  6381  ordtr2  6401  funopsnOLD  7144  tpres  7199  funfvima  7228  isomin  7337  sorpsscmpl  7739  peano5  7894  resf1ext2b  7936  f1oweALT  7973  poxp  8129  soxp  8130  tfr3  8391  tz7.48-1  8437  omordi  8558  odi  8571  omass  8572  oen0  8579  nndi  8616  nnmass  8617  nnmordi  8624  eroveu  8817  ssfi  9172  findcard3  9258  fiint  9302  suplub  9436  hartogs  9522  card2on  9532  unxpwdom2  9566  inf3lem2  9614  ttrclselem2  9711  epfrs  9716  tcel  9728  frr3g  9744  dfac2b  10190  infpssr  10367  isf32lem9  10420  axdc3lem4  10512  axcclem  10516  zorn2lem7  10561  ttukeylem6  10573  brdom6disj  10592  ondomon  10628  inar1  10841  gruen  10878  indpi  10973  nqereu  10995  genpn0  11069  distrlem1pr  11091  distrlem5pr  11093  ltexprlem1  11102  reclem4pr  11116  addsrmo  11139  mulsrmo  11140  supsrlem  11177  lelttr  11381  ltlen  11392  fzind  12778  xrlelttr  13266  xnn0xaddcl  13346  fzen  13654  bernneq  14353  swrdswrdlem  14833  repsdf2  14909  limsupbnd2  15630  mulcn2  15743  prodmolem2  16082  dvdsmod0  16408  lcmfunsnlem1  16792  divgcdcoprm0  16820  maxprmfct  16865  pceu  17004  dvdsprmpweqnn  17043  oddprmdvds  17061  infpnlem1  17068  prmgaplem6  17214  imasaddfnlem  17680  initoeu1  18166  termoeu1  18173  plelttr  18496  gsumval2a  18854  cycsubm  19397  symgfix2  19610  psgnunilem4  19691  lsmmod  19869  efgrelexlemb  19944  imasabl  20070  pgpfac1lem5  20275  rngqiprngimf1lem  21570  rngqiprngimfo  21577  ssdifidlprm  21622  nzerooringczr  21766  lindfrn  22107  mat1dimcrng  22772  dmatelnd  22791  mdetunilem7  22913  cpmatacl  23014  cpmatmcllem  23016  lmss  23596  hausnei2  23651  isnrm2  23656  isnrm3  23657  cmpsublem  23697  2ndcdisj  23755  txcnpi  23907  tx1stc  23949  fgcl  24177  ufileu  24218  fmfnfmlem4  24256  fmfnfm  24257  alexsubALTlem4  24349  alexsubALT  24350  tmdgsum2  24395  prdsxmslem2  24828  ovolicc2  25823  volfiniun  25848  dyadmax  25899  ellimc3  26179  dvlip2  26295  dvne0  26311  dvfsumlem2  26327  taylthlem2  26683  zabsle1  27605  2lgslem3  27713  2sqreulem3  27762  ltlesnd  28114  cutsun12  28158  mulsproplem9  28492  mulsprop  28498  bdayons  28644  n0ssoldg  28721  eucliddivs  28744  bdayfinbndlem1  28835  axcontlem4  29527  uhgr2edg  29771  ushgredgedg  29792  ushgredgedgloop  29794  nb3grprlem1  29943  rusgr1vtx  30151  wlkonl1iedg  30226  uhgrwkspthlem2  30322  usgr2wlkneq  30324  usgr2trlncl  30328  uspgrn2crct  30379  wspthsnonn0vne  30488  usgrwwlks2on  30529  umgrwwlks2on  30530  elwspths2on  30533  elwspths2onw  30534  clwlkclwwlkf1lem3  30579  erclwwlktr  30595  erclwwlkntr  30644  frgrnbnb  30876  frgr2wwlk1  30912  frrusgrord  30924  wlkl0  30950  isch3  31825  ocin  31880  shmodsi  31973  spansneleq  32154  stj  32819  atom1d  32937  atcvat2i  32971  chirredlem1  32974  chirredi  32978  mdsymlem3  32989  mdsymlem6  32992  bnj849  35538  fineqvinfep  35766  pconnconn  35965  cvmsss2  36008  cvmliftlem7  36025  satfv0  36092  satfv0fun  36105  satffunlem  36135  satffunlem1lem1  36136  satffunlem2lem1  36138  mclsind  36304  dfon2lem9  36523  dfon2  36524  cgrextend  36743  btwntriv2  36747  btwncomim  36748  btwnexch3  36755  funtransport  36766  ifscgr  36779  colinearxfr  36810  lineext  36811  fscgr  36815  outsideoftr  36864  nmuladdss  36932  trer  37074  finminlem  37076  fnessref  37115  fgmin  37128  axnulregtco  37238  bj-andnotim  37428  bj-alanim  37467  bj-axreprepsep  37959  bj-0int  37990  relowlssretop  38254  finorwe  38273  finxpsuclem  38288  wl-ax13lem1  38385  poimirlem29  38535  itg2addnclem3  38559  itg2addnc  38560  areacirc  38599  ismtybndlem  38708  heibor1lem  38711  iss2  39244  disjlem17  39802  membpartlem19  39814  prtlem17  39901  riotasvd  39981  lshpsmreu  40134  atnle  40342  cvratlem  40446  cvrat2  40454  3dim1  40492  2llnjN  40592  2lplnj  40645  linepsubN  40777  pmapsub  40793  paddasslem14  40858  pclfinN  40925  ispsubcl2N  40972  pclfinclN  40975  ldilval  41138  trlord  41594  cdlemk36  41938  dihlsscpre  42259  baerlem3lem2  42735  baerlem5alem2  42736  baerlem5blem2  42737  pellexlem5  43793  pellex  43795  pell1234qrmulcl  43815  pellfundex  43846  cantnfresb  44284  omabs2  44292  relexpmulnn  44668  clsk1indlem3  45002  19.41rg  45492  iunconnlem2  45876  relpmin  45894  or2expropbi  48048  fcoresf1  48083  euoreqb  48123  2reu8i  48127  dfatcolem  48269  f1oresf1o2  48305  nltle2tri  48327  imasetpreimafvbijlemf1  48430  iccpartnel  48464  ich2exprop  48497  ichreuopeq  48499  paireqne  48537  prprelprb  48543  reupr  48548  reuopreuprim  48552  nprmmul3  48555  fmtnofac2lem  48597  sfprmdvdsmersenne  48632  lighneallem3  48636  lighneallem4  48639  requad2  48665  bgoldbtbnd  48851  dfnbgr6  48899  isubgredg  48908  grimuhgr  48929  grimco  48931  uhgrimedgi  48932  isuspgrimlem  48937  clnbgrgrimlem  48975  grimedg  48977  gpgvtxedg0  49105  gpgvtxedg1  49106  gpgedg2ov  49108  gpgedg2iv  49109  pgnbgreunbgrlem1  49155  pgnbgreunbgrlem2lem1  49156  pgnbgreunbgrlem2lem2  49157  pgnbgreunbgrlem2lem3  49158  pgnbgreunbgrlem2  49159  pgnbgreunbgrlem3  49160  pgnbgreunbgrlem4  49161  pgnbgreunbgrlem5  49165  pgnbgreunbgrlem6  49166  pgnbgreunbgr  49167  upgrwlkupwlk  49182  ldepspr  49529  affinecomb1  49758  itsclc0  49827  aacllem  50883