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 206  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  602  3expib  1121  ax13lem1  2372  equs5  2458  rsp2  3273  moi  3714  reu6  3722  sbciegft  3815  ss2abdv  4060  elpwunsn  4687  opthpr  4852  preqsnd  4859  opthprneg  4865  3elpr2eq  4907  invdisj  5132  snopeqop  5506  solin  5613  sotr2  5620  wefrc  5670  relop  5850  elinxp  6019  reuop  6292  dfpo2  6295  tz7.7  6390  ordtr2  6408  funopsn  7148  tpres  7204  funfvima  7234  isomin  7337  sorpsscmpl  7728  peano5  7888  peano5OLD  7889  f1oweALT  7963  poxp  8119  soxp  8120  tfr3  8405  tz7.48-1  8449  omordi  8572  odi  8585  omass  8586  oen0  8592  nndi  8629  nnmass  8630  nnmordi  8637  eroveu  8812  ssfi  9179  findcard3  9291  findcard3OLD  9292  fiint  9330  suplub  9461  hartogs  9545  card2on  9555  unxpwdom2  9589  inf3lem2  9630  ttrclselem2  9727  epfrs  9732  tcel  9746  frr3g  9757  dfac2b  10131  infpssr  10309  isf32lem9  10362  axdc3lem4  10454  axcclem  10458  zorn2lem7  10503  ttukeylem6  10515  brdom6disj  10533  ondomon  10564  inar1  10776  gruen  10813  indpi  10908  nqereu  10930  genpn0  11004  distrlem1pr  11026  distrlem5pr  11028  ltexprlem1  11037  reclem4pr  11051  addsrmo  11074  mulsrmo  11075  supsrlem  11112  lelttr  11311  ltlen  11322  mulgt1  12080  fzind  12667  xrlelttr  13142  xnn0xaddcl  13221  fzen  13525  bernneq  14199  swrdswrdlem  14661  repsdf2  14735  limsupbnd2  15434  mulcn2  15547  prodmolem2  15886  dvdsmod0  16210  lcmfunsnlem1  16581  divgcdcoprm0  16609  maxprmfct  16653  pceu  16786  dvdsprmpweqnn  16825  oddprmdvds  16843  infpnlem1  16850  prmgaplem6  16996  imasaddfnlem  17481  initoeu1  17968  termoeu1  17975  plelttr  18304  gsumval2a  18613  cycsubm  19121  symgfix2  19329  psgnunilem4  19410  lsmmod  19588  efgrelexlemb  19663  imasabl  19789  pgpfac1lem5  19994  rngqiprngimf1lem  21057  rngqiprngimfo  21064  lindfrn  21599  mat1dimcrng  22212  dmatelnd  22231  mdetunilem7  22353  cpmatacl  22451  cpmatmcllem  22453  lmss  23035  hausnei2  23090  isnrm2  23095  isnrm3  23096  cmpsublem  23136  2ndcdisj  23193  txcnpi  23345  tx1stc  23387  fgcl  23615  ufileu  23656  fmfnfmlem4  23694  fmfnfm  23695  alexsubALTlem4  23787  alexsubALT  23788  tmdgsum2  23833  prdsxmslem2  24271  ovolicc2  25284  volfiniun  25309  dyadmax  25360  ellimc3  25641  dvlip2  25761  dvne0  25777  zabsle1  27050  2lgslem3  27158  2sqreulem3  27207  scutun12  27563  mulsproplem9  27834  mulsprop  27840  axcontlem4  28507  uhgr2edg  28747  ushgredgedg  28768  ushgredgedgloop  28770  nb3grprlem1  28919  rusgr1vtx  29127  wlkonl1iedg  29204  uhgrwkspthlem2  29293  usgr2wlkneq  29295  usgr2trlncl  29299  uspgrn2crct  29344  wspthsnonn0vne  29453  umgrwwlks2on  29493  elwspths2on  29496  clwlkclwwlkf1lem3  29541  erclwwlktr  29557  erclwwlkntr  29606  frgrnbnb  29828  frgr2wwlk1  29864  frrusgrord  29876  wlkl0  29902  isch3  30776  ocin  30831  shmodsi  30924  spansneleq  31105  stj  31770  atom1d  31888  atcvat2i  31922  chirredlem1  31925  chirredi  31929  mdsymlem3  31940  mdsymlem6  31943  bnj849  34249  pconnconn  34535  cvmsss2  34578  cvmliftlem7  34595  satfv0  34662  satfv0fun  34675  satffunlem  34705  satffunlem1lem1  34706  satffunlem2lem1  34708  mclsind  34874  dfon2lem9  35082  dfon2  35083  cgrextend  35299  btwntriv2  35303  btwncomim  35304  btwnexch3  35311  funtransport  35322  ifscgr  35335  colinearxfr  35366  lineext  35367  fscgr  35371  outsideoftr  35420  gg-dvfsumlem2  35480  trer  35517  finminlem  35519  fnessref  35558  fgmin  35571  bj-andnotim  35782  bj-alanim  35806  bj-0int  36298  relowlssretop  36560  finorwe  36579  finxpsuclem  36594  wl-ax13lem1  36691  poimirlem29  36833  itg2addnclem3  36857  itg2addnc  36858  areacirc  36897  ismtybndlem  36990  heibor1lem  36993  iss2  37529  disjlem17  37985  membpartlem19  37997  prtlem17  38062  riotasvd  38142  lshpsmreu  38295  atnle  38503  cvratlem  38608  cvrat2  38616  3dim1  38654  2llnjN  38754  2lplnj  38807  linepsubN  38939  pmapsub  38955  paddasslem14  39020  pclfinN  39087  ispsubcl2N  39134  pclfinclN  39137  ldilval  39300  trlord  39756  cdlemk36  40100  dihlsscpre  40421  baerlem3lem2  40897  baerlem5alem2  40898  baerlem5blem2  40899  pellexlem5  41886  pellex  41888  pell1234qrmulcl  41908  pellfundex  41939  cantnfresb  42389  omabs2  42397  relexpmulnn  42775  clsk1indlem3  43109  19.41rg  43626  iunconnlem2  44011  or2expropbi  46055  fcoresf1  46090  euoreqb  46128  2reu8i  46132  dfatcolem  46274  f1oresf1o2  46310  nltle2tri  46332  imasetpreimafvbijlemf1  46383  iccpartnel  46417  ich2exprop  46450  ichreuopeq  46452  paireqne  46490  prprelprb  46496  reupr  46501  reuopreuprim  46505  fmtnofac2lem  46547  sfprmdvdsmersenne  46582  lighneallem3  46586  lighneallem4  46589  requad2  46602  bgoldbtbnd  46788  isomuspgrlem2d  46810  isomgrsym  46815  isomgrtr  46818  upgrwlkupwlk  46829  nzerooringczr  47071  ldepspr  47254  affinecomb1  47488  itsclc0  47557  aacllem  47948