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  2377  equs5  2463  rsp2  3263  moi  3708  reu6  3716  sbciegftOLD  3810  elpwunsn  4666  opthpr  4833  preqsnd  4841  opthprneg  4847  3elpr2eq  4888  invdisj  5111  snopeqop  5493  solin  5601  sotr2  5608  wefrc  5661  relop  5843  elinxp  6019  reuop  6295  dfpo2  6298  tz7.7  6391  ordtr2  6409  funopsn  7149  tpres  7204  funfvima  7233  isomin  7340  sorpsscmpl  7737  peano5  7898  resf1ext2b  7940  f1oweALT  7980  poxp  8136  soxp  8137  tfr3  8422  tz7.48-1  8466  omordi  8587  odi  8600  omass  8601  oen0  8607  nndi  8644  nnmass  8645  nnmordi  8652  eroveu  8835  ssfi  9196  findcard3  9301  findcard3OLD  9302  fiint  9349  fiintOLD  9350  suplub  9483  hartogs  9567  card2on  9577  unxpwdom2  9611  inf3lem2  9652  ttrclselem2  9749  epfrs  9754  tcel  9768  frr3g  9779  dfac2b  10154  infpssr  10331  isf32lem9  10384  axdc3lem4  10476  axcclem  10480  zorn2lem7  10525  ttukeylem6  10537  brdom6disj  10555  ondomon  10586  inar1  10798  gruen  10835  indpi  10930  nqereu  10952  genpn0  11026  distrlem1pr  11048  distrlem5pr  11050  ltexprlem1  11059  reclem4pr  11073  addsrmo  11096  mulsrmo  11097  supsrlem  11134  lelttr  11334  ltlen  11345  mulgt1OLD  12109  fzind  12700  xrlelttr  13181  xnn0xaddcl  13260  fzen  13564  bernneq  14251  swrdswrdlem  14725  repsdf2  14799  limsupbnd2  15502  mulcn2  15615  prodmolem2  15954  dvdsmod0  16279  lcmfunsnlem1  16657  divgcdcoprm0  16685  maxprmfct  16729  pceu  16867  dvdsprmpweqnn  16906  oddprmdvds  16924  infpnlem1  16931  prmgaplem6  17077  imasaddfnlem  17549  initoeu1  18032  termoeu1  18039  plelttr  18363  gsumval2a  18672  cycsubm  19194  symgfix2  19407  psgnunilem4  19488  lsmmod  19666  efgrelexlemb  19741  imasabl  19867  pgpfac1lem5  20072  rngqiprngimf1lem  21271  rngqiprngimfo  21278  nzerooringczr  21458  lindfrn  21808  mat1dimcrng  22450  dmatelnd  22469  mdetunilem7  22591  cpmatacl  22689  cpmatmcllem  22691  lmss  23271  hausnei2  23326  isnrm2  23331  isnrm3  23332  cmpsublem  23372  2ndcdisj  23429  txcnpi  23581  tx1stc  23623  fgcl  23851  ufileu  23892  fmfnfmlem4  23930  fmfnfm  23931  alexsubALTlem4  24023  alexsubALT  24024  tmdgsum2  24069  prdsxmslem2  24505  ovolicc2  25512  volfiniun  25537  dyadmax  25588  ellimc3  25869  dvlip2  25989  dvne0  26005  dvfsumlem2  26022  taylthlem2  26371  zabsle1  27295  2lgslem3  27403  2sqreulem3  27452  sltlend  27771  scutun12  27810  mulsproplem9  28105  mulsprop  28111  axcontlem4  28931  uhgr2edg  29172  ushgredgedg  29193  ushgredgedgloop  29195  nb3grprlem1  29344  rusgr1vtx  29553  wlkonl1iedg  29630  uhgrwkspthlem2  29721  usgr2wlkneq  29723  usgr2trlncl  29727  uspgrn2crct  29775  wspthsnonn0vne  29884  umgrwwlks2on  29924  elwspths2on  29927  clwlkclwwlkf1lem3  29972  erclwwlktr  29988  erclwwlkntr  30037  frgrnbnb  30259  frgr2wwlk1  30295  frrusgrord  30307  wlkl0  30333  isch3  31207  ocin  31262  shmodsi  31355  spansneleq  31536  stj  32201  atom1d  32319  atcvat2i  32353  chirredlem1  32356  chirredi  32360  mdsymlem3  32371  mdsymlem6  32374  ssdifidlprm  33427  bnj849  34880  pconnconn  35177  cvmsss2  35220  cvmliftlem7  35237  satfv0  35304  satfv0fun  35317  satffunlem  35347  satffunlem1lem1  35348  satffunlem2lem1  35350  mclsind  35516  dfon2lem9  35733  dfon2  35734  cgrextend  35950  btwntriv2  35954  btwncomim  35955  btwnexch3  35962  funtransport  35973  ifscgr  35986  colinearxfr  36017  lineext  36018  fscgr  36022  outsideoftr  36071  trer  36258  finminlem  36260  fnessref  36299  fgmin  36312  bj-andnotim  36530  bj-alanim  36554  bj-0int  37043  relowlssretop  37305  finorwe  37324  finxpsuclem  37339  wl-ax13lem1  37436  poimirlem29  37597  itg2addnclem3  37621  itg2addnc  37622  areacirc  37661  ismtybndlem  37754  heibor1lem  37757  iss2  38286  disjlem17  38741  membpartlem19  38753  prtlem17  38818  riotasvd  38898  lshpsmreu  39051  atnle  39259  cvratlem  39364  cvrat2  39372  3dim1  39410  2llnjN  39510  2lplnj  39563  linepsubN  39695  pmapsub  39711  paddasslem14  39776  pclfinN  39843  ispsubcl2N  39890  pclfinclN  39893  ldilval  40056  trlord  40512  cdlemk36  40856  dihlsscpre  41177  baerlem3lem2  41653  baerlem5alem2  41654  baerlem5blem2  41655  pellexlem5  42789  pellex  42791  pell1234qrmulcl  42811  pellfundex  42842  cantnfresb  43282  omabs2  43290  relexpmulnn  43667  clsk1indlem3  44001  19.41rg  44515  iunconnlem2  44900  relpmin  44918  or2expropbi  46992  fcoresf1  47027  euoreqb  47067  2reu8i  47071  dfatcolem  47213  f1oresf1o2  47249  nltle2tri  47271  imasetpreimafvbijlemf1  47337  iccpartnel  47371  ich2exprop  47404  ichreuopeq  47406  paireqne  47444  prprelprb  47450  reupr  47455  reuopreuprim  47459  fmtnofac2lem  47501  sfprmdvdsmersenne  47536  lighneallem3  47540  lighneallem4  47543  requad2  47556  bgoldbtbnd  47742  dfnbgr6  47789  isubgredg  47798  isuspgrimlem  47820  grimuhgr  47824  grimco  47826  clnbgrgrimlem  47847  grimedg  47849  gpgvtxedg0  47967  gpgvtxedg1  47968  upgrwlkupwlk  48002  ldepspr  48336  affinecomb1  48569  itsclc0  48638  aacllem  49316