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  2406  equs5  2492  rsp2  3283  moi  3679  reu6  3687  elpwunsn  4645  opthpr  4809  preqsnd  4817  opthprneg  4823  3elpr2eq  4837  invdisj  5092  snopeqop  5482  solin  5590  sotr2  5597  wefrc  5649  relop  5834  elinxp  6020  reuop  6314  dfpo2  6317  tz7.7  6406  ordtr2  6426  funopsnOLD  7176  tpres  7230  funfvima  7259  isomin  7368  sorpsscmpl  7774  peano5  7929  resf1ext2b  7971  f1oweALT  8008  poxp  8167  soxp  8168  tfr3  8435  tz7.48-1  8481  omordi  8602  odi  8615  omass  8616  oen0  8623  nndi  8660  nnmass  8661  nnmordi  8668  eroveu  8861  ssfi  9216  findcard3  9302  fiint  9346  suplub  9479  hartogs  9565  card2on  9575  unxpwdom2  9609  inf3lem2  9657  ttrclselem2  9754  epfrs  9759  tcel  9771  frr3g  9787  dfac2b  10236  infpssr  10413  isf32lem9  10466  axdc3lem4  10558  axcclem  10562  zorn2lem7  10607  ttukeylem6  10619  brdom6disj  10638  ondomon  10674  inar1  10887  gruen  10924  indpi  11019  nqereu  11041  genpn0  11115  distrlem1pr  11137  distrlem5pr  11139  ltexprlem1  11148  reclem4pr  11162  addsrmo  11185  mulsrmo  11186  supsrlem  11223  lelttr  11427  ltlen  11438  fzind  12824  xrlelttr  13312  xnn0xaddcl  13392  fzen  13701  bernneq  14400  swrdswrdlem  14881  repsdf2  14957  limsupbnd2  15679  mulcn2  15792  prodmolem2  16131  dvdsmod0  16457  lcmfunsnlem1  16841  divgcdcoprm0  16869  maxprmfct  16914  pceu  17053  dvdsprmpweqnn  17092  oddprmdvds  17110  infpnlem1  17117  prmgaplem6  17263  imasaddfnlem  17729  initoeu1  18215  termoeu1  18222  plelttr  18545  gsumval2a  18903  cycsubm  19446  symgfix2  19660  psgnunilem4  19741  lsmmod  19919  efgrelexlemb  19994  imasabl  20120  pgpfac1lem5  20325  rngqiprngimf1lem  21620  rngqiprngimfo  21627  ssdifidlprm  21672  nzerooringczr  21816  lindfrn  22157  mat1dimcrng  22822  dmatelnd  22841  mdetunilem7  22963  cpmatacl  23064  cpmatmcllem  23066  lmss  23646  hausnei2  23701  isnrm2  23706  isnrm3  23707  cmpsublem  23747  2ndcdisj  23805  txcnpi  23957  tx1stc  23999  fgcl  24227  ufileu  24268  fmfnfmlem4  24306  fmfnfm  24307  alexsubALTlem4  24399  alexsubALT  24400  tmdgsum2  24445  prdsxmslem2  24878  ovolicc2  25873  volfiniun  25898  dyadmax  25949  ellimc3  26229  dvlip2  26345  dvne0  26361  dvfsumlem2  26377  taylthlem2  26731  zabsle1  27653  2lgslem3  27761  2sqreulem3  27810  ltlesnd  28162  cutsun12  28206  mulsproplem9  28540  mulsprop  28546  bdayons  28692  n0ssoldg  28769  eucliddivs  28792  bdayfinbndlem1  28883  axcontlem4  29575  uhgr2edg  29819  ushgredgedg  29840  ushgredgedgloop  29842  nb3grprlem1  29991  rusgr1vtx  30199  wlkonl1iedg  30274  uhgrwkspthlem2  30370  usgr2wlkneq  30372  usgr2trlncl  30376  uspgrn2crct  30427  wspthsnonn0vne  30536  usgrwwlks2on  30577  umgrwwlks2on  30578  elwspths2on  30581  elwspths2onw  30582  clwlkclwwlkf1lem3  30627  erclwwlktr  30643  erclwwlkntr  30692  frgrnbnb  30924  frgr2wwlk1  30960  frrusgrord  30972  wlkl0  30998  isch3  31873  ocin  31928  shmodsi  32021  spansneleq  32202  stj  32867  atom1d  32985  atcvat2i  33019  chirredlem1  33022  chirredi  33026  mdsymlem3  33037  mdsymlem6  33040  bnj849  35625  reu6f  35779  soinfdom  35800  fineqvinfep  35893  pconnconn  36163  cvmsss2  36206  cvmliftlem7  36223  satfv0  36290  satfv0fun  36303  satffunlem  36333  satffunlem1lem1  36334  satffunlem2lem1  36336  mclsind  36502  dfon2lem9  36731  dfon2  36732  cgrextend  36951  btwntriv2  36955  btwncomim  36956  btwnexch3  36963  funtransport  36974  ifscgr  36987  colinearxfr  37018  lineext  37019  fscgr  37023  outsideoftr  37072  nmuladdss  37140  trer  37282  finminlem  37284  fnessref  37323  fgmin  37336  axnulregtco  37446  bj-andnotim  37636  bj-alanim  37675  bj-axreprepsep  38182  bj-0int  38213  relowlssretop  38478  finorwe  38497  finxpsuclem  38512  wl-ax13lem1  38609  poimirlem29  38759  itg2addnclem3  38783  itg2addnc  38784  areacirc  38823  ismtybndlem  38932  heibor1lem  38935  iss2  39468  disjlem17  40026  membpartlem19  40038  prtlem17  40125  riotasvd  40205  lshpsmreu  40358  atnle  40566  cvratlem  40670  cvrat2  40678  3dim1  40716  2llnjN  40816  2lplnj  40869  linepsubN  41001  pmapsub  41017  paddasslem14  41082  pclfinN  41149  ispsubcl2N  41196  pclfinclN  41199  ldilval  41362  trlord  41818  cdlemk36  42162  dihlsscpre  42483  baerlem3lem2  42959  baerlem5alem2  42960  baerlem5blem2  42961  pellexlem5  44033  pellex  44035  pell1234qrmulcl  44055  pellfundex  44086  cantnfresb  44518  omabs2  44526  relexpmulnn  44901  clsk1indlem3  45235  19.41rg  45724  iunconnlem2  46108  cocanss2  46114  relpmin  46137  or2expropbi  48309  fcoresf1  48344  euoreqb  48385  2reu8i  48389  dfatcolem  48530  f1oresf1o2  48566  nltle2tri  48588  imasetpreimafvbijlemf1  48691  iccpartnel  48725  ich2exprop  48758  ichreuopeq  48760  paireqne  48798  prprelprb  48804  reupr  48809  reuopreuprim  48813  nprmmul3  48816  fmtnofac2lem  48858  sfprmdvdsmersenne  48893  lighneallem3  48897  lighneallem4  48900  requad2  48926  bgoldbtbnd  49112  dfnbgr6  49160  isubgredg  49169  grimuhgr  49190  grimco  49192  uhgrimedgi  49193  isuspgrimlem  49198  clnbgrgrimlem  49236  grimedg  49238  gpgvtxedg0  49366  gpgvtxedg1  49367  gpgedg2ov  49369  gpgedg2iv  49370  pgnbgreunbgrlem1  49416  pgnbgreunbgrlem2lem1  49417  pgnbgreunbgrlem2lem2  49418  pgnbgreunbgrlem2lem3  49419  pgnbgreunbgrlem2  49420  pgnbgreunbgrlem3  49421  pgnbgreunbgrlem4  49422  pgnbgreunbgrlem5  49426  pgnbgreunbgrlem6  49427  pgnbgreunbgr  49428  upgrwlkupwlk  49443  ldepspr  49790  affinecomb1  50019  itsclc0  50088  aacllem  51219