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  2374  equs5  2460  rsp2  3249  moi  3677  reu6  3685  sbciegftOLD  3779  elpwunsn  4637  opthpr  4803  preqsnd  4811  opthprneg  4817  3elpr2eq  4858  invdisj  5077  snopeqop  5446  solin  5551  sotr2  5558  wefrc  5610  relop  5790  elinxp  5968  reuop  6240  dfpo2  6243  tz7.7  6332  ordtr2  6351  funopsn  7081  tpres  7135  funfvima  7164  isomin  7271  sorpsscmpl  7667  peano5  7823  resf1ext2b  7865  f1oweALT  7904  poxp  8058  soxp  8059  tfr3  8318  tz7.48-1  8362  omordi  8481  odi  8494  omass  8495  oen0  8501  nndi  8538  nnmass  8539  nnmordi  8546  eroveu  8736  ssfi  9082  findcard3  9167  fiint  9211  suplub  9344  hartogs  9430  card2on  9440  unxpwdom2  9474  inf3lem2  9519  ttrclselem2  9616  epfrs  9621  tcel  9633  frr3g  9649  dfac2b  10022  infpssr  10199  isf32lem9  10252  axdc3lem4  10344  axcclem  10348  zorn2lem7  10393  ttukeylem6  10405  brdom6disj  10423  ondomon  10454  inar1  10666  gruen  10703  indpi  10798  nqereu  10820  genpn0  10894  distrlem1pr  10916  distrlem5pr  10918  ltexprlem1  10927  reclem4pr  10941  addsrmo  10964  mulsrmo  10965  supsrlem  11002  lelttr  11203  ltlen  11214  mulgt1OLD  11980  fzind  12571  xrlelttr  13055  xnn0xaddcl  13134  fzen  13441  bernneq  14136  swrdswrdlem  14611  repsdf2  14685  limsupbnd2  15390  mulcn2  15503  prodmolem2  15842  dvdsmod0  16169  lcmfunsnlem1  16548  divgcdcoprm0  16576  maxprmfct  16620  pceu  16758  dvdsprmpweqnn  16797  oddprmdvds  16815  infpnlem1  16822  prmgaplem6  16968  imasaddfnlem  17432  initoeu1  17918  termoeu1  17925  plelttr  18248  gsumval2a  18593  cycsubm  19115  symgfix2  19329  psgnunilem4  19410  lsmmod  19588  efgrelexlemb  19663  imasabl  19789  pgpfac1lem5  19994  rngqiprngimf1lem  21232  rngqiprngimfo  21239  nzerooringczr  21418  lindfrn  21759  mat1dimcrng  22393  dmatelnd  22412  mdetunilem7  22534  cpmatacl  22632  cpmatmcllem  22634  lmss  23214  hausnei2  23269  isnrm2  23274  isnrm3  23275  cmpsublem  23315  2ndcdisj  23372  txcnpi  23524  tx1stc  23566  fgcl  23794  ufileu  23835  fmfnfmlem4  23873  fmfnfm  23874  alexsubALTlem4  23966  alexsubALT  23967  tmdgsum2  24012  prdsxmslem2  24445  ovolicc2  25451  volfiniun  25476  dyadmax  25527  ellimc3  25808  dvlip2  25928  dvne0  25944  dvfsumlem2  25961  taylthlem2  26310  zabsle1  27235  2lgslem3  27343  2sqreulem3  27392  sltlend  27711  scutun12  27752  mulsproplem9  28064  mulsprop  28070  bdayon  28210  eucliddivs  28302  axcontlem4  28946  uhgr2edg  29187  ushgredgedg  29208  ushgredgedgloop  29210  nb3grprlem1  29359  rusgr1vtx  29568  wlkonl1iedg  29643  uhgrwkspthlem2  29733  usgr2wlkneq  29735  usgr2trlncl  29739  uspgrn2crct  29787  wspthsnonn0vne  29896  umgrwwlks2on  29936  elwspths2on  29939  clwlkclwwlkf1lem3  29984  erclwwlktr  30000  erclwwlkntr  30049  frgrnbnb  30271  frgr2wwlk1  30307  frrusgrord  30319  wlkl0  30345  isch3  31219  ocin  31274  shmodsi  31367  spansneleq  31548  stj  32213  atom1d  32331  atcvat2i  32365  chirredlem1  32368  chirredi  32372  mdsymlem3  32383  mdsymlem6  32386  ssdifidlprm  33421  bnj849  34935  pconnconn  35273  cvmsss2  35316  cvmliftlem7  35333  satfv0  35400  satfv0fun  35413  satffunlem  35443  satffunlem1lem1  35444  satffunlem2lem1  35446  mclsind  35612  dfon2lem9  35831  dfon2  35832  cgrextend  36048  btwntriv2  36052  btwncomim  36053  btwnexch3  36060  funtransport  36071  ifscgr  36084  colinearxfr  36115  lineext  36116  fscgr  36120  outsideoftr  36169  trer  36356  finminlem  36358  fnessref  36397  fgmin  36410  bj-andnotim  36628  bj-alanim  36652  bj-0int  37141  relowlssretop  37403  finorwe  37422  finxpsuclem  37437  wl-ax13lem1  37534  poimirlem29  37695  itg2addnclem3  37719  itg2addnc  37720  areacirc  37759  ismtybndlem  37852  heibor1lem  37855  iss2  38378  disjlem17  38843  membpartlem19  38855  prtlem17  38921  riotasvd  39001  lshpsmreu  39154  atnle  39362  cvratlem  39466  cvrat2  39474  3dim1  39512  2llnjN  39612  2lplnj  39665  linepsubN  39797  pmapsub  39813  paddasslem14  39878  pclfinN  39945  ispsubcl2N  39992  pclfinclN  39995  ldilval  40158  trlord  40614  cdlemk36  40958  dihlsscpre  41279  baerlem3lem2  41755  baerlem5alem2  41756  baerlem5blem2  41757  pellexlem5  42872  pellex  42874  pell1234qrmulcl  42894  pellfundex  42925  cantnfresb  43363  omabs2  43371  relexpmulnn  43748  clsk1indlem3  44082  19.41rg  44589  iunconnlem2  44973  relpmin  44991  or2expropbi  47071  fcoresf1  47106  euoreqb  47146  2reu8i  47150  dfatcolem  47292  f1oresf1o2  47328  nltle2tri  47350  imasetpreimafvbijlemf1  47441  iccpartnel  47475  ich2exprop  47508  ichreuopeq  47510  paireqne  47548  prprelprb  47554  reupr  47559  reuopreuprim  47563  fmtnofac2lem  47605  sfprmdvdsmersenne  47640  lighneallem3  47644  lighneallem4  47647  requad2  47660  bgoldbtbnd  47846  dfnbgr6  47894  isubgredg  47903  grimuhgr  47924  grimco  47926  uhgrimedgi  47927  isuspgrimlem  47932  clnbgrgrimlem  47970  grimedg  47972  gpgvtxedg0  48100  gpgvtxedg1  48101  gpgedg2ov  48103  gpgedg2iv  48104  pgnbgreunbgrlem1  48150  pgnbgreunbgrlem2lem1  48151  pgnbgreunbgrlem2lem2  48152  pgnbgreunbgrlem2lem3  48153  pgnbgreunbgrlem2  48154  pgnbgreunbgrlem3  48155  pgnbgreunbgrlem4  48156  pgnbgreunbgrlem5  48160  pgnbgreunbgrlem6  48161  pgnbgreunbgr  48162  upgrwlkupwlk  48177  ldepspr  48511  affinecomb1  48740  itsclc0  48809  aacllem  49839