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  604  3expib  1123  ax13lem1  2379  equs5  2465  rsp2  3255  moi  3678  reu6  3686  sbciegftOLD  3780  elpwunsn  4643  opthpr  4809  preqsnd  4817  opthprneg  4823  3elpr2eq  4864  invdisj  5086  snopeqop  5462  solin  5567  sotr2  5574  wefrc  5626  relop  5807  elinxp  5986  reuop  6259  dfpo2  6262  tz7.7  6351  ordtr2  6370  funopsn  7103  tpres  7157  funfvima  7186  isomin  7293  sorpsscmpl  7689  peano5  7845  resf1ext2b  7887  f1oweALT  7926  poxp  8080  soxp  8081  tfr3  8340  tz7.48-1  8384  omordi  8503  odi  8516  omass  8517  oen0  8524  nndi  8561  nnmass  8562  nnmordi  8569  eroveu  8761  ssfi  9109  findcard3  9195  fiint  9239  suplub  9375  hartogs  9461  card2on  9471  unxpwdom2  9505  inf3lem2  9550  ttrclselem2  9647  epfrs  9652  tcel  9664  frr3g  9680  dfac2b  10053  infpssr  10230  isf32lem9  10283  axdc3lem4  10375  axcclem  10379  zorn2lem7  10424  ttukeylem6  10436  brdom6disj  10454  ondomon  10485  inar1  10698  gruen  10735  indpi  10830  nqereu  10852  genpn0  10926  distrlem1pr  10948  distrlem5pr  10950  ltexprlem1  10959  reclem4pr  10973  addsrmo  10996  mulsrmo  10997  supsrlem  11034  lelttr  11235  ltlen  11246  mulgt1OLD  12012  fzind  12602  xrlelttr  13082  xnn0xaddcl  13162  fzen  13469  bernneq  14164  swrdswrdlem  14639  repsdf2  14713  limsupbnd2  15418  mulcn2  15531  prodmolem2  15870  dvdsmod0  16197  lcmfunsnlem1  16576  divgcdcoprm0  16604  maxprmfct  16648  pceu  16786  dvdsprmpweqnn  16825  oddprmdvds  16843  infpnlem1  16850  prmgaplem6  16996  imasaddfnlem  17461  initoeu1  17947  termoeu1  17954  plelttr  18277  gsumval2a  18622  cycsubm  19143  symgfix2  19357  psgnunilem4  19438  lsmmod  19616  efgrelexlemb  19691  imasabl  19817  pgpfac1lem5  20022  rngqiprngimf1lem  21261  rngqiprngimfo  21268  nzerooringczr  21447  lindfrn  21788  mat1dimcrng  22433  dmatelnd  22452  mdetunilem7  22574  cpmatacl  22672  cpmatmcllem  22674  lmss  23254  hausnei2  23309  isnrm2  23314  isnrm3  23315  cmpsublem  23355  2ndcdisj  23412  txcnpi  23564  tx1stc  23606  fgcl  23834  ufileu  23875  fmfnfmlem4  23913  fmfnfm  23914  alexsubALTlem4  24006  alexsubALT  24007  tmdgsum2  24052  prdsxmslem2  24485  ovolicc2  25491  volfiniun  25516  dyadmax  25567  ellimc3  25848  dvlip2  25968  dvne0  25984  dvfsumlem2  26001  taylthlem2  26350  zabsle1  27275  2lgslem3  27383  2sqreulem3  27432  ltlesnd  27755  cutsun12  27798  mulsproplem9  28132  mulsprop  28138  bdayons  28284  n0ssoldg  28361  eucliddivs  28384  bdayfinbndlem1  28475  axcontlem4  29052  uhgr2edg  29293  ushgredgedg  29314  ushgredgedgloop  29316  nb3grprlem1  29465  rusgr1vtx  29674  wlkonl1iedg  29749  uhgrwkspthlem2  29839  usgr2wlkneq  29841  usgr2trlncl  29845  uspgrn2crct  29893  wspthsnonn0vne  30002  usgrwwlks2on  30043  umgrwwlks2on  30044  elwspths2on  30047  elwspths2onw  30048  clwlkclwwlkf1lem3  30093  erclwwlktr  30109  erclwwlkntr  30158  frgrnbnb  30380  frgr2wwlk1  30416  frrusgrord  30428  wlkl0  30454  isch3  31328  ocin  31383  shmodsi  31476  spansneleq  31657  stj  32322  atom1d  32440  atcvat2i  32474  chirredlem1  32477  chirredi  32481  mdsymlem3  32492  mdsymlem6  32495  ssdifidlprm  33550  bnj849  35100  fineqvinfep  35300  pconnconn  35444  cvmsss2  35487  cvmliftlem7  35504  satfv0  35571  satfv0fun  35584  satffunlem  35614  satffunlem1lem1  35615  satffunlem2lem1  35617  mclsind  35783  dfon2lem9  36002  dfon2  36003  cgrextend  36221  btwntriv2  36225  btwncomim  36226  btwnexch3  36233  funtransport  36244  ifscgr  36257  colinearxfr  36288  lineext  36289  fscgr  36293  outsideoftr  36342  trer  36529  finminlem  36531  fnessref  36570  fgmin  36583  bj-andnotim  36810  bj-alanim  36847  bj-axreprepsep  37320  bj-0int  37351  relowlssretop  37615  finorwe  37634  finxpsuclem  37649  wl-ax13lem1  37746  poimirlem29  37897  itg2addnclem3  37921  itg2addnc  37922  areacirc  37961  ismtybndlem  38054  heibor1lem  38057  iss2  38592  disjlem17  39150  membpartlem19  39162  prtlem17  39249  riotasvd  39329  lshpsmreu  39482  atnle  39690  cvratlem  39794  cvrat2  39802  3dim1  39840  2llnjN  39940  2lplnj  39993  linepsubN  40125  pmapsub  40141  paddasslem14  40206  pclfinN  40273  ispsubcl2N  40320  pclfinclN  40323  ldilval  40486  trlord  40942  cdlemk36  41286  dihlsscpre  41607  baerlem3lem2  42083  baerlem5alem2  42084  baerlem5blem2  42085  pellexlem5  43187  pellex  43189  pell1234qrmulcl  43209  pellfundex  43240  cantnfresb  43678  omabs2  43686  relexpmulnn  44062  clsk1indlem3  44396  19.41rg  44903  iunconnlem2  45287  relpmin  45305  or2expropbi  47391  fcoresf1  47426  euoreqb  47466  2reu8i  47470  dfatcolem  47612  f1oresf1o2  47648  nltle2tri  47670  imasetpreimafvbijlemf1  47761  iccpartnel  47795  ich2exprop  47828  ichreuopeq  47830  paireqne  47868  prprelprb  47874  reupr  47879  reuopreuprim  47883  fmtnofac2lem  47925  sfprmdvdsmersenne  47960  lighneallem3  47964  lighneallem4  47967  requad2  47980  bgoldbtbnd  48166  dfnbgr6  48214  isubgredg  48223  grimuhgr  48244  grimco  48246  uhgrimedgi  48247  isuspgrimlem  48252  clnbgrgrimlem  48290  grimedg  48292  gpgvtxedg0  48420  gpgvtxedg1  48421  gpgedg2ov  48423  gpgedg2iv  48424  pgnbgreunbgrlem1  48470  pgnbgreunbgrlem2lem1  48471  pgnbgreunbgrlem2lem2  48472  pgnbgreunbgrlem2lem3  48473  pgnbgreunbgrlem2  48474  pgnbgreunbgrlem3  48475  pgnbgreunbgrlem4  48476  pgnbgreunbgrlem5  48480  pgnbgreunbgrlem6  48481  pgnbgreunbgr  48482  upgrwlkupwlk  48497  ldepspr  48830  affinecomb1  49059  itsclc0  49128  aacllem  50157