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  602  3expib  1122  ax13lem1  2382  equs5  2468  rsp2  3283  moi  3740  reu6  3748  sbciegftOLD  3843  elpwunsn  4707  opthpr  4876  preqsnd  4883  opthprneg  4889  3elpr2eq  4930  invdisj  5152  snopeqop  5525  solin  5634  sotr2  5641  wefrc  5694  relop  5875  elinxp  6048  reuop  6324  dfpo2  6327  tz7.7  6421  ordtr2  6439  funopsn  7182  tpres  7238  funfvima  7267  isomin  7373  sorpsscmpl  7769  peano5  7932  peano5OLD  7933  f1oweALT  8013  poxp  8169  soxp  8170  tfr3  8455  tz7.48-1  8499  omordi  8622  odi  8635  omass  8636  oen0  8642  nndi  8679  nnmass  8680  nnmordi  8687  eroveu  8870  ssfi  9240  findcard3  9346  findcard3OLD  9347  fiint  9394  fiintOLD  9395  suplub  9529  hartogs  9613  card2on  9623  unxpwdom2  9657  inf3lem2  9698  ttrclselem2  9795  epfrs  9800  tcel  9814  frr3g  9825  dfac2b  10200  infpssr  10377  isf32lem9  10430  axdc3lem4  10522  axcclem  10526  zorn2lem7  10571  ttukeylem6  10583  brdom6disj  10601  ondomon  10632  inar1  10844  gruen  10881  indpi  10976  nqereu  10998  genpn0  11072  distrlem1pr  11094  distrlem5pr  11096  ltexprlem1  11105  reclem4pr  11119  addsrmo  11142  mulsrmo  11143  supsrlem  11180  lelttr  11380  ltlen  11391  mulgt1OLD  12153  fzind  12741  xrlelttr  13218  xnn0xaddcl  13297  fzen  13601  bernneq  14278  swrdswrdlem  14752  repsdf2  14826  limsupbnd2  15529  mulcn2  15642  prodmolem2  15983  dvdsmod0  16308  lcmfunsnlem1  16684  divgcdcoprm0  16712  maxprmfct  16756  pceu  16893  dvdsprmpweqnn  16932  oddprmdvds  16950  infpnlem1  16957  prmgaplem6  17103  imasaddfnlem  17588  initoeu1  18078  termoeu1  18085  plelttr  18414  gsumval2a  18723  cycsubm  19242  symgfix2  19458  psgnunilem4  19539  lsmmod  19717  efgrelexlemb  19792  imasabl  19918  pgpfac1lem5  20123  rngqiprngimf1lem  21327  rngqiprngimfo  21334  nzerooringczr  21514  lindfrn  21864  mat1dimcrng  22504  dmatelnd  22523  mdetunilem7  22645  cpmatacl  22743  cpmatmcllem  22745  lmss  23327  hausnei2  23382  isnrm2  23387  isnrm3  23388  cmpsublem  23428  2ndcdisj  23485  txcnpi  23637  tx1stc  23679  fgcl  23907  ufileu  23948  fmfnfmlem4  23986  fmfnfm  23987  alexsubALTlem4  24079  alexsubALT  24080  tmdgsum2  24125  prdsxmslem2  24563  ovolicc2  25576  volfiniun  25601  dyadmax  25652  ellimc3  25934  dvlip2  26054  dvne0  26070  dvfsumlem2  26087  taylthlem2  26434  zabsle1  27358  2lgslem3  27466  2sqreulem3  27515  sltlend  27834  scutun12  27873  mulsproplem9  28168  mulsprop  28174  axcontlem4  29000  uhgr2edg  29243  ushgredgedg  29264  ushgredgedgloop  29266  nb3grprlem1  29415  rusgr1vtx  29624  wlkonl1iedg  29701  uhgrwkspthlem2  29790  usgr2wlkneq  29792  usgr2trlncl  29796  uspgrn2crct  29841  wspthsnonn0vne  29950  umgrwwlks2on  29990  elwspths2on  29993  clwlkclwwlkf1lem3  30038  erclwwlktr  30054  erclwwlkntr  30103  frgrnbnb  30325  frgr2wwlk1  30361  frrusgrord  30373  wlkl0  30399  isch3  31273  ocin  31328  shmodsi  31421  spansneleq  31602  stj  32267  atom1d  32385  atcvat2i  32419  chirredlem1  32422  chirredi  32426  mdsymlem3  32437  mdsymlem6  32440  ssdifidlprm  33451  bnj849  34901  pconnconn  35199  cvmsss2  35242  cvmliftlem7  35259  satfv0  35326  satfv0fun  35339  satffunlem  35369  satffunlem1lem1  35370  satffunlem2lem1  35372  mclsind  35538  dfon2lem9  35755  dfon2  35756  cgrextend  35972  btwntriv2  35976  btwncomim  35977  btwnexch3  35984  funtransport  35995  ifscgr  36008  colinearxfr  36039  lineext  36040  fscgr  36044  outsideoftr  36093  trer  36282  finminlem  36284  fnessref  36323  fgmin  36336  bj-andnotim  36554  bj-alanim  36578  bj-0int  37067  relowlssretop  37329  finorwe  37348  finxpsuclem  37363  wl-ax13lem1  37460  poimirlem29  37609  itg2addnclem3  37633  itg2addnc  37634  areacirc  37673  ismtybndlem  37766  heibor1lem  37769  iss2  38300  disjlem17  38755  membpartlem19  38767  prtlem17  38832  riotasvd  38912  lshpsmreu  39065  atnle  39273  cvratlem  39378  cvrat2  39386  3dim1  39424  2llnjN  39524  2lplnj  39577  linepsubN  39709  pmapsub  39725  paddasslem14  39790  pclfinN  39857  ispsubcl2N  39904  pclfinclN  39907  ldilval  40070  trlord  40526  cdlemk36  40870  dihlsscpre  41191  baerlem3lem2  41667  baerlem5alem2  41668  baerlem5blem2  41669  pellexlem5  42789  pellex  42791  pell1234qrmulcl  42811  pellfundex  42842  cantnfresb  43286  omabs2  43294  relexpmulnn  43671  clsk1indlem3  44005  19.41rg  44521  iunconnlem2  44906  or2expropbi  46949  fcoresf1  46984  euoreqb  47024  2reu8i  47028  dfatcolem  47170  f1oresf1o2  47206  nltle2tri  47228  imasetpreimafvbijlemf1  47278  iccpartnel  47312  ich2exprop  47345  ichreuopeq  47347  paireqne  47385  prprelprb  47391  reupr  47396  reuopreuprim  47400  fmtnofac2lem  47442  sfprmdvdsmersenne  47477  lighneallem3  47481  lighneallem4  47484  requad2  47497  bgoldbtbnd  47683  dfnbgr6  47729  isuspgrimlem  47758  grimuhgr  47762  grimco  47764  clnbgrgrimlem  47785  grimedg  47787  upgrwlkupwlk  47863  ldepspr  48202  affinecomb1  48436  itsclc0  48505  aacllem  48895