Theorem impd 410

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 89	. . 3 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	imp 406	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
4	3	com12 32	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  impcomd  411  imp32  418  imp4b  421  imp4c  423  imp4d  424  imp5d  439  imp5g  441  pm3.31  449  expimpd  453  expl  457  ancomsd  465  syland  602  3expib  1120  ax13lem1  2369  equs5  2455  rsp2  3270  moi  3712  reu6  3720  sbciegft  3813  ss2abdv  4057  elpwunsn  4684  opthpr  4849  preqsnd  4856  opthprneg  4862  3elpr2eq  4903  invdisj  5127  snopeqop  5503  solin  5610  sotr2  5617  wefrc  5667  relop  5848  elinxp  6018  reuop  6292  dfpo2  6295  tz7.7  6390  ordtr2  6408  funopsn  7152  tpres  7208  funfvima  7237  isomin  7340  sorpsscmpl  7734  peano5  7894  peano5OLD  7895  f1oweALT  7971  poxp  8128  soxp  8129  tfr3  8414  tz7.48-1  8458  omordi  8581  odi  8594  omass  8595  oen0  8601  nndi  8638  nnmass  8639  nnmordi  8646  eroveu  8825  ssfi  9192  findcard3  9304  findcard3OLD  9305  fiint  9343  suplub  9478  hartogs  9562  card2on  9572  unxpwdom2  9606  inf3lem2  9647  ttrclselem2  9744  epfrs  9749  tcel  9763  frr3g  9774  dfac2b  10148  infpssr  10326  isf32lem9  10379  axdc3lem4  10471  axcclem  10475  zorn2lem7  10520  ttukeylem6  10532  brdom6disj  10550  ondomon  10581  inar1  10793  gruen  10830  indpi  10925  nqereu  10947  genpn0  11021  distrlem1pr  11043  distrlem5pr  11045  ltexprlem1  11054  reclem4pr  11068  addsrmo  11091  mulsrmo  11092  supsrlem  11129  lelttr  11329  ltlen  11340  mulgt1  12098  fzind  12685  xrlelttr  13162  xnn0xaddcl  13241  fzen  13545  bernneq  14218  swrdswrdlem  14681  repsdf2  14755  limsupbnd2  15454  mulcn2  15567  prodmolem2  15906  dvdsmod0  16231  lcmfunsnlem1  16602  divgcdcoprm0  16630  maxprmfct  16674  pceu  16809  dvdsprmpweqnn  16848  oddprmdvds  16866  infpnlem1  16873  prmgaplem6  17019  imasaddfnlem  17504  initoeu1  17994  termoeu1  18001  plelttr  18330  gsumval2a  18639  cycsubm  19151  symgfix2  19365  psgnunilem4  19446  lsmmod  19624  efgrelexlemb  19699  imasabl  19825  pgpfac1lem5  20030  rngqiprngimf1lem  21178  rngqiprngimfo  21185  nzerooringczr  21400  lindfrn  21749  mat1dimcrng  22373  dmatelnd  22392  mdetunilem7  22514  cpmatacl  22612  cpmatmcllem  22614  lmss  23196  hausnei2  23251  isnrm2  23256  isnrm3  23257  cmpsublem  23297  2ndcdisj  23354  txcnpi  23506  tx1stc  23548  fgcl  23776  ufileu  23817  fmfnfmlem4  23855  fmfnfm  23856  alexsubALTlem4  23948  alexsubALT  23949  tmdgsum2  23994  prdsxmslem2  24432  ovolicc2  25445  volfiniun  25470  dyadmax  25521  ellimc3  25802  dvlip2  25922  dvne0  25938  dvfsumlem2  25955  taylthlem2  26303  zabsle1  27223  2lgslem3  27331  2sqreulem3  27380  sltlend  27698  scutun12  27737  mulsproplem9  28018  mulsprop  28024  axcontlem4  28772  uhgr2edg  29015  ushgredgedg  29036  ushgredgedgloop  29038  nb3grprlem1  29187  rusgr1vtx  29396  wlkonl1iedg  29473  uhgrwkspthlem2  29562  usgr2wlkneq  29564  usgr2trlncl  29568  uspgrn2crct  29613  wspthsnonn0vne  29722  umgrwwlks2on  29762  elwspths2on  29765  clwlkclwwlkf1lem3  29810  erclwwlktr  29826  erclwwlkntr  29875  frgrnbnb  30097  frgr2wwlk1  30133  frrusgrord  30145  wlkl0  30171  isch3  31045  ocin  31100  shmodsi  31193  spansneleq  31374  stj  32039  atom1d  32157  atcvat2i  32191  chirredlem1  32194  chirredi  32198  mdsymlem3  32209  mdsymlem6  32212  bnj849  34551  pconnconn  34836  cvmsss2  34879  cvmliftlem7  34896  satfv0  34963  satfv0fun  34976  satffunlem  35006  satffunlem1lem1  35007  satffunlem2lem1  35009  mclsind  35175  dfon2lem9  35382  dfon2  35383  cgrextend  35599  btwntriv2  35603  btwncomim  35604  btwnexch3  35611  funtransport  35622  ifscgr  35635  colinearxfr  35666  lineext  35667  fscgr  35671  outsideoftr  35720  trer  35795  finminlem  35797  fnessref  35836  fgmin  35849  bj-andnotim  36060  bj-alanim  36084  bj-0int  36575  relowlssretop  36837  finorwe  36856  finxpsuclem  36871  wl-ax13lem1  36968  poimirlem29  37117  itg2addnclem3  37141  itg2addnc  37142  areacirc  37181  ismtybndlem  37274  heibor1lem  37277  iss2  37811  disjlem17  38266  membpartlem19  38278  prtlem17  38343  riotasvd  38423  lshpsmreu  38576  atnle  38784  cvratlem  38889  cvrat2  38897  3dim1  38935  2llnjN  39035  2lplnj  39088  linepsubN  39220  pmapsub  39236  paddasslem14  39301  pclfinN  39368  ispsubcl2N  39415  pclfinclN  39418  ldilval  39581  trlord  40037  cdlemk36  40381  dihlsscpre  40702  baerlem3lem2  41178  baerlem5alem2  41179  baerlem5blem2  41180  pellexlem5  42244  pellex  42246  pell1234qrmulcl  42266  pellfundex  42297  cantnfresb  42744  omabs2  42752  relexpmulnn  43130  clsk1indlem3  43464  19.41rg  43980  iunconnlem2  44365  or2expropbi  46407  fcoresf1  46442  euoreqb  46480  2reu8i  46484  dfatcolem  46626  f1oresf1o2  46662  nltle2tri  46684  imasetpreimafvbijlemf1  46735  iccpartnel  46769  ich2exprop  46802  ichreuopeq  46804  paireqne  46842  prprelprb  46848  reupr  46853  reuopreuprim  46857  fmtnofac2lem  46899  sfprmdvdsmersenne  46934  lighneallem3  46938  lighneallem4  46941  requad2  46954  bgoldbtbnd  47140  isuspgrimlem  47163  grimuhgr  47167  grimco  47169  upgrwlkupwlk  47193  ldepspr  47532  affinecomb1  47766  itsclc0  47835  aacllem  48225