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  2376  equs5  2462  rsp2  3250  moi  3673  reu6  3681  sbciegftOLD  3775  elpwunsn  4636  opthpr  4802  preqsnd  4810  opthprneg  4816  3elpr2eq  4857  invdisj  5079  snopeqop  5449  solin  5554  sotr2  5561  wefrc  5613  relop  5794  elinxp  5972  reuop  6245  dfpo2  6248  tz7.7  6337  ordtr2  6356  funopsn  7087  tpres  7141  funfvima  7170  isomin  7277  sorpsscmpl  7673  peano5  7829  resf1ext2b  7871  f1oweALT  7910  poxp  8064  soxp  8065  tfr3  8324  tz7.48-1  8368  omordi  8487  odi  8500  omass  8501  oen0  8507  nndi  8544  nnmass  8545  nnmordi  8552  eroveu  8742  ssfi  9089  findcard3  9174  fiint  9218  suplub  9351  hartogs  9437  card2on  9447  unxpwdom2  9481  inf3lem2  9526  ttrclselem2  9623  epfrs  9628  tcel  9640  frr3g  9656  dfac2b  10029  infpssr  10206  isf32lem9  10259  axdc3lem4  10351  axcclem  10355  zorn2lem7  10400  ttukeylem6  10412  brdom6disj  10430  ondomon  10461  inar1  10673  gruen  10710  indpi  10805  nqereu  10827  genpn0  10901  distrlem1pr  10923  distrlem5pr  10925  ltexprlem1  10934  reclem4pr  10948  addsrmo  10971  mulsrmo  10972  supsrlem  11009  lelttr  11210  ltlen  11221  mulgt1OLD  11987  fzind  12577  xrlelttr  13057  xnn0xaddcl  13136  fzen  13443  bernneq  14138  swrdswrdlem  14613  repsdf2  14687  limsupbnd2  15392  mulcn2  15505  prodmolem2  15844  dvdsmod0  16171  lcmfunsnlem1  16550  divgcdcoprm0  16578  maxprmfct  16622  pceu  16760  dvdsprmpweqnn  16799  oddprmdvds  16817  infpnlem1  16824  prmgaplem6  16970  imasaddfnlem  17434  initoeu1  17920  termoeu1  17927  plelttr  18250  gsumval2a  18595  cycsubm  19116  symgfix2  19330  psgnunilem4  19411  lsmmod  19589  efgrelexlemb  19664  imasabl  19790  pgpfac1lem5  19995  rngqiprngimf1lem  21233  rngqiprngimfo  21240  nzerooringczr  21419  lindfrn  21760  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  28947  uhgr2edg  29188  ushgredgedg  29209  ushgredgedgloop  29211  nb3grprlem1  29360  rusgr1vtx  29569  wlkonl1iedg  29644  uhgrwkspthlem2  29734  usgr2wlkneq  29736  usgr2trlncl  29740  uspgrn2crct  29788  wspthsnonn0vne  29897  usgrwwlks2on  29938  umgrwwlks2on  29939  elwspths2on  29942  elwspths2onw  29943  clwlkclwwlkf1lem3  29988  erclwwlktr  30004  erclwwlkntr  30053  frgrnbnb  30275  frgr2wwlk1  30311  frrusgrord  30323  wlkl0  30349  isch3  31223  ocin  31278  shmodsi  31371  spansneleq  31552  stj  32217  atom1d  32335  atcvat2i  32369  chirredlem1  32372  chirredi  32376  mdsymlem3  32387  mdsymlem6  32390  ssdifidlprm  33430  bnj849  34958  pconnconn  35296  cvmsss2  35339  cvmliftlem7  35356  satfv0  35423  satfv0fun  35436  satffunlem  35466  satffunlem1lem1  35467  satffunlem2lem1  35469  mclsind  35635  dfon2lem9  35854  dfon2  35855  cgrextend  36073  btwntriv2  36077  btwncomim  36078  btwnexch3  36085  funtransport  36096  ifscgr  36109  colinearxfr  36140  lineext  36141  fscgr  36145  outsideoftr  36194  trer  36381  finminlem  36383  fnessref  36422  fgmin  36435  bj-andnotim  36653  bj-alanim  36677  bj-0int  37166  relowlssretop  37428  finorwe  37447  finxpsuclem  37462  wl-ax13lem1  37559  poimirlem29  37710  itg2addnclem3  37734  itg2addnc  37735  areacirc  37774  ismtybndlem  37867  heibor1lem  37870  iss2  38397  disjlem17  38918  membpartlem19  38930  prtlem17  38996  riotasvd  39076  lshpsmreu  39229  atnle  39437  cvratlem  39541  cvrat2  39549  3dim1  39587  2llnjN  39687  2lplnj  39740  linepsubN  39872  pmapsub  39888  paddasslem14  39953  pclfinN  40020  ispsubcl2N  40067  pclfinclN  40070  ldilval  40233  trlord  40689  cdlemk36  41033  dihlsscpre  41354  baerlem3lem2  41830  baerlem5alem2  41831  baerlem5blem2  41832  pellexlem5  42951  pellex  42953  pell1234qrmulcl  42973  pellfundex  43004  cantnfresb  43442  omabs2  43450  relexpmulnn  43827  clsk1indlem3  44161  19.41rg  44668  iunconnlem2  45052  relpmin  45070  or2expropbi  47159  fcoresf1  47194  euoreqb  47234  2reu8i  47238  dfatcolem  47380  f1oresf1o2  47416  nltle2tri  47438  imasetpreimafvbijlemf1  47529  iccpartnel  47563  ich2exprop  47596  ichreuopeq  47598  paireqne  47636  prprelprb  47642  reupr  47647  reuopreuprim  47651  fmtnofac2lem  47693  sfprmdvdsmersenne  47728  lighneallem3  47732  lighneallem4  47735  requad2  47748  bgoldbtbnd  47934  dfnbgr6  47982  isubgredg  47991  grimuhgr  48012  grimco  48014  uhgrimedgi  48015  isuspgrimlem  48020  clnbgrgrimlem  48058  grimedg  48060  gpgvtxedg0  48188  gpgvtxedg1  48189  gpgedg2ov  48191  gpgedg2iv  48192  pgnbgreunbgrlem1  48238  pgnbgreunbgrlem2lem1  48239  pgnbgreunbgrlem2lem2  48240  pgnbgreunbgrlem2lem3  48241  pgnbgreunbgrlem2  48242  pgnbgreunbgrlem3  48243  pgnbgreunbgrlem4  48244  pgnbgreunbgrlem5  48248  pgnbgreunbgrlem6  48249  pgnbgreunbgr  48250  upgrwlkupwlk  48265  ldepspr  48599  affinecomb1  48828  itsclc0  48897  aacllem  49927