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  2378  equs5  2464  rsp2  3254  moi  3664  reu6  3672  sbciegftOLD  3766  elpwunsn  4628  opthpr  4794  preqsnd  4802  opthprneg  4808  3elpr2eq  4849  invdisj  5071  snopeqop  5460  solin  5566  sotr2  5573  wefrc  5625  relop  5805  elinxp  5984  reuop  6257  dfpo2  6260  tz7.7  6349  ordtr2  6368  funopsnOLD  7102  tpres  7156  funfvima  7185  isomin  7292  sorpsscmpl  7688  peano5  7844  resf1ext2b  7886  f1oweALT  7925  poxp  8078  soxp  8079  tfr3  8338  tz7.48-1  8382  omordi  8501  odi  8514  omass  8515  oen0  8522  nndi  8559  nnmass  8560  nnmordi  8567  eroveu  8759  ssfi  9107  findcard3  9193  fiint  9237  suplub  9373  hartogs  9459  card2on  9469  unxpwdom2  9503  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  11236  ltlen  11247  mulgt1OLD  12014  fzind  12627  xrlelttr  13107  xnn0xaddcl  13187  fzen  13495  bernneq  14191  swrdswrdlem  14666  repsdf2  14740  limsupbnd2  15445  mulcn2  15558  prodmolem2  15900  dvdsmod0  16227  lcmfunsnlem1  16606  divgcdcoprm0  16634  maxprmfct  16679  pceu  16817  dvdsprmpweqnn  16856  oddprmdvds  16874  infpnlem1  16881  prmgaplem6  17027  imasaddfnlem  17492  initoeu1  17978  termoeu1  17985  plelttr  18308  gsumval2a  18653  cycsubm  19177  symgfix2  19391  psgnunilem4  19472  lsmmod  19650  efgrelexlemb  19725  imasabl  19851  pgpfac1lem5  20056  rngqiprngimf1lem  21292  rngqiprngimfo  21299  nzerooringczr  21460  lindfrn  21801  mat1dimcrng  22442  dmatelnd  22461  mdetunilem7  22583  cpmatacl  22681  cpmatmcllem  22683  lmss  23263  hausnei2  23318  isnrm2  23323  isnrm3  23324  cmpsublem  23364  2ndcdisj  23421  txcnpi  23573  tx1stc  23615  fgcl  23843  ufileu  23884  fmfnfmlem4  23922  fmfnfm  23923  alexsubALTlem4  24015  alexsubALT  24016  tmdgsum2  24061  prdsxmslem2  24494  ovolicc2  25489  volfiniun  25514  dyadmax  25565  ellimc3  25846  dvlip2  25962  dvne0  25978  dvfsumlem2  25994  taylthlem2  26339  zabsle1  27259  2lgslem3  27367  2sqreulem3  27416  ltlesnd  27739  cutsun12  27782  mulsproplem9  28116  mulsprop  28122  bdayons  28268  n0ssoldg  28345  eucliddivs  28368  bdayfinbndlem1  28459  axcontlem4  29036  uhgr2edg  29277  ushgredgedg  29298  ushgredgedgloop  29300  nb3grprlem1  29449  rusgr1vtx  29657  wlkonl1iedg  29732  uhgrwkspthlem2  29822  usgr2wlkneq  29824  usgr2trlncl  29828  uspgrn2crct  29876  wspthsnonn0vne  29985  usgrwwlks2on  30026  umgrwwlks2on  30027  elwspths2on  30030  elwspths2onw  30031  clwlkclwwlkf1lem3  30076  erclwwlktr  30092  erclwwlkntr  30141  frgrnbnb  30363  frgr2wwlk1  30399  frrusgrord  30411  wlkl0  30437  isch3  31312  ocin  31367  shmodsi  31460  spansneleq  31641  stj  32306  atom1d  32424  atcvat2i  32458  chirredlem1  32461  chirredi  32465  mdsymlem3  32476  mdsymlem6  32479  ssdifidlprm  33518  bnj849  35067  fineqvinfep  35269  pconnconn  35413  cvmsss2  35456  cvmliftlem7  35473  satfv0  35540  satfv0fun  35553  satffunlem  35583  satffunlem1lem1  35584  satffunlem2lem1  35586  mclsind  35752  dfon2lem9  35971  dfon2  35972  cgrextend  36190  btwntriv2  36194  btwncomim  36195  btwnexch3  36202  funtransport  36213  ifscgr  36226  colinearxfr  36257  lineext  36258  fscgr  36262  outsideoftr  36311  trer  36498  finminlem  36500  fnessref  36539  fgmin  36552  axnulregtco  36662  bj-andnotim  36853  bj-alanim  36892  bj-axreprepsep  37382  bj-0int  37413  relowlssretop  37679  finorwe  37698  finxpsuclem  37713  wl-ax13lem1  37810  poimirlem29  37970  itg2addnclem3  37994  itg2addnc  37995  areacirc  38034  ismtybndlem  38127  heibor1lem  38130  iss2  38665  disjlem17  39223  membpartlem19  39235  prtlem17  39322  riotasvd  39402  lshpsmreu  39555  atnle  39763  cvratlem  39867  cvrat2  39875  3dim1  39913  2llnjN  40013  2lplnj  40066  linepsubN  40198  pmapsub  40214  paddasslem14  40279  pclfinN  40346  ispsubcl2N  40393  pclfinclN  40396  ldilval  40559  trlord  41015  cdlemk36  41359  dihlsscpre  41680  baerlem3lem2  42156  baerlem5alem2  42157  baerlem5blem2  42158  pellexlem5  43261  pellex  43263  pell1234qrmulcl  43283  pellfundex  43314  cantnfresb  43752  omabs2  43760  relexpmulnn  44136  clsk1indlem3  44470  19.41rg  44977  iunconnlem2  45361  relpmin  45379  or2expropbi  47482  fcoresf1  47517  euoreqb  47557  2reu8i  47561  dfatcolem  47703  f1oresf1o2  47739  nltle2tri  47761  imasetpreimafvbijlemf1  47864  iccpartnel  47898  ich2exprop  47931  ichreuopeq  47933  paireqne  47971  prprelprb  47977  reupr  47982  reuopreuprim  47986  nprmmul3  47989  fmtnofac2lem  48031  sfprmdvdsmersenne  48066  lighneallem3  48070  lighneallem4  48073  requad2  48099  bgoldbtbnd  48285  dfnbgr6  48333  isubgredg  48342  grimuhgr  48363  grimco  48365  uhgrimedgi  48366  isuspgrimlem  48371  clnbgrgrimlem  48409  grimedg  48411  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgedg2ov  48542  gpgedg2iv  48543  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem2  48593  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5  48599  pgnbgreunbgrlem6  48600  pgnbgreunbgr  48601  upgrwlkupwlk  48616  ldepspr  48949  affinecomb1  49178  itsclc0  49247  aacllem  50276