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 207  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  603  3expib  1122  ax13lem1  2379  equs5  2465  rsp2  3263  moi  3706  reu6  3714  sbciegftOLD  3808  elpwunsn  4665  opthpr  4832  preqsnd  4840  opthprneg  4846  3elpr2eq  4887  invdisj  5110  snopeqop  5486  solin  5593  sotr2  5600  wefrc  5653  relop  5835  elinxp  6011  reuop  6287  dfpo2  6290  tz7.7  6383  ordtr2  6402  funopsn  7143  tpres  7198  funfvima  7227  isomin  7335  sorpsscmpl  7733  peano5  7894  resf1ext2b  7936  f1oweALT  7976  poxp  8132  soxp  8133  tfr3  8418  tz7.48-1  8462  omordi  8583  odi  8596  omass  8597  oen0  8603  nndi  8640  nnmass  8641  nnmordi  8648  eroveu  8831  ssfi  9192  findcard3  9295  findcard3OLD  9296  fiint  9343  fiintOLD  9344  suplub  9477  hartogs  9563  card2on  9573  unxpwdom2  9607  inf3lem2  9648  ttrclselem2  9745  epfrs  9750  tcel  9764  frr3g  9775  dfac2b  10150  infpssr  10327  isf32lem9  10380  axdc3lem4  10472  axcclem  10476  zorn2lem7  10521  ttukeylem6  10533  brdom6disj  10551  ondomon  10582  inar1  10794  gruen  10831  indpi  10926  nqereu  10948  genpn0  11022  distrlem1pr  11044  distrlem5pr  11046  ltexprlem1  11055  reclem4pr  11069  addsrmo  11092  mulsrmo  11093  supsrlem  11130  lelttr  11330  ltlen  11341  mulgt1OLD  12105  fzind  12696  xrlelttr  13177  xnn0xaddcl  13256  fzen  13563  bernneq  14252  swrdswrdlem  14727  repsdf2  14801  limsupbnd2  15504  mulcn2  15617  prodmolem2  15956  dvdsmod0  16283  lcmfunsnlem1  16661  divgcdcoprm0  16689  maxprmfct  16733  pceu  16871  dvdsprmpweqnn  16910  oddprmdvds  16928  infpnlem1  16935  prmgaplem6  17081  imasaddfnlem  17547  initoeu1  18029  termoeu1  18036  plelttr  18359  gsumval2a  18668  cycsubm  19190  symgfix2  19402  psgnunilem4  19483  lsmmod  19661  efgrelexlemb  19736  imasabl  19862  pgpfac1lem5  20067  rngqiprngimf1lem  21260  rngqiprngimfo  21267  nzerooringczr  21446  lindfrn  21786  mat1dimcrng  22420  dmatelnd  22439  mdetunilem7  22561  cpmatacl  22659  cpmatmcllem  22661  lmss  23241  hausnei2  23296  isnrm2  23301  isnrm3  23302  cmpsublem  23342  2ndcdisj  23399  txcnpi  23551  tx1stc  23593  fgcl  23821  ufileu  23862  fmfnfmlem4  23900  fmfnfm  23901  alexsubALTlem4  23993  alexsubALT  23994  tmdgsum2  24039  prdsxmslem2  24473  ovolicc2  25480  volfiniun  25505  dyadmax  25556  ellimc3  25837  dvlip2  25957  dvne0  25973  dvfsumlem2  25990  taylthlem2  26339  zabsle1  27264  2lgslem3  27372  2sqreulem3  27421  sltlend  27740  scutun12  27779  mulsproplem9  28084  mulsprop  28090  bdayon  28230  eucliddivs  28322  axcontlem4  28951  uhgr2edg  29192  ushgredgedg  29213  ushgredgedgloop  29215  nb3grprlem1  29364  rusgr1vtx  29573  wlkonl1iedg  29650  uhgrwkspthlem2  29741  usgr2wlkneq  29743  usgr2trlncl  29747  uspgrn2crct  29795  wspthsnonn0vne  29904  umgrwwlks2on  29944  elwspths2on  29947  clwlkclwwlkf1lem3  29992  erclwwlktr  30008  erclwwlkntr  30057  frgrnbnb  30279  frgr2wwlk1  30315  frrusgrord  30327  wlkl0  30353  isch3  31227  ocin  31282  shmodsi  31375  spansneleq  31556  stj  32221  atom1d  32339  atcvat2i  32373  chirredlem1  32376  chirredi  32380  mdsymlem3  32391  mdsymlem6  32394  ssdifidlprm  33478  bnj849  34961  pconnconn  35258  cvmsss2  35301  cvmliftlem7  35318  satfv0  35385  satfv0fun  35398  satffunlem  35428  satffunlem1lem1  35429  satffunlem2lem1  35431  mclsind  35597  dfon2lem9  35814  dfon2  35815  cgrextend  36031  btwntriv2  36035  btwncomim  36036  btwnexch3  36043  funtransport  36054  ifscgr  36067  colinearxfr  36098  lineext  36099  fscgr  36103  outsideoftr  36152  trer  36339  finminlem  36341  fnessref  36380  fgmin  36393  bj-andnotim  36611  bj-alanim  36635  bj-0int  37124  relowlssretop  37386  finorwe  37405  finxpsuclem  37420  wl-ax13lem1  37517  poimirlem29  37678  itg2addnclem3  37702  itg2addnc  37703  areacirc  37742  ismtybndlem  37835  heibor1lem  37838  iss2  38367  disjlem17  38822  membpartlem19  38834  prtlem17  38899  riotasvd  38979  lshpsmreu  39132  atnle  39340  cvratlem  39445  cvrat2  39453  3dim1  39491  2llnjN  39591  2lplnj  39644  linepsubN  39776  pmapsub  39792  paddasslem14  39857  pclfinN  39924  ispsubcl2N  39971  pclfinclN  39974  ldilval  40137  trlord  40593  cdlemk36  40937  dihlsscpre  41258  baerlem3lem2  41734  baerlem5alem2  41735  baerlem5blem2  41736  pellexlem5  42831  pellex  42833  pell1234qrmulcl  42853  pellfundex  42884  cantnfresb  43323  omabs2  43331  relexpmulnn  43708  clsk1indlem3  44042  19.41rg  44550  iunconnlem2  44934  relpmin  44952  or2expropbi  47043  fcoresf1  47078  euoreqb  47118  2reu8i  47122  dfatcolem  47264  f1oresf1o2  47300  nltle2tri  47322  imasetpreimafvbijlemf1  47398  iccpartnel  47432  ich2exprop  47465  ichreuopeq  47467  paireqne  47505  prprelprb  47511  reupr  47516  reuopreuprim  47520  fmtnofac2lem  47562  sfprmdvdsmersenne  47597  lighneallem3  47601  lighneallem4  47604  requad2  47617  bgoldbtbnd  47803  dfnbgr6  47850  isubgredg  47859  grimuhgr  47880  grimco  47882  uhgrimedgi  47883  isuspgrimlem  47888  clnbgrgrimlem  47926  grimedg  47928  gpgvtxedg0  48047  gpgvtxedg1  48048  upgrwlkupwlk  48095  ldepspr  48429  affinecomb1  48662  itsclc0  48731  aacllem  49645