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  2378  equs5  2464  rsp2  3253  moi  3676  reu6  3684  sbciegftOLD  3778  elpwunsn  4641  opthpr  4807  preqsnd  4815  opthprneg  4821  3elpr2eq  4862  invdisj  5084  snopeqop  5454  solin  5559  sotr2  5566  wefrc  5618  relop  5799  elinxp  5978  reuop  6251  dfpo2  6254  tz7.7  6343  ordtr2  6362  funopsn  7093  tpres  7147  funfvima  7176  isomin  7283  sorpsscmpl  7679  peano5  7835  resf1ext2b  7877  f1oweALT  7916  poxp  8070  soxp  8071  tfr3  8330  tz7.48-1  8374  omordi  8493  odi  8506  omass  8507  oen0  8514  nndi  8551  nnmass  8552  nnmordi  8559  eroveu  8749  ssfi  9097  findcard3  9183  fiint  9227  suplub  9363  hartogs  9449  card2on  9459  unxpwdom2  9493  inf3lem2  9538  ttrclselem2  9635  epfrs  9640  tcel  9652  frr3g  9668  dfac2b  10041  infpssr  10218  isf32lem9  10271  axdc3lem4  10363  axcclem  10367  zorn2lem7  10412  ttukeylem6  10424  brdom6disj  10442  ondomon  10473  inar1  10686  gruen  10723  indpi  10818  nqereu  10840  genpn0  10914  distrlem1pr  10936  distrlem5pr  10938  ltexprlem1  10947  reclem4pr  10961  addsrmo  10984  mulsrmo  10985  supsrlem  11022  lelttr  11223  ltlen  11234  mulgt1OLD  12000  fzind  12590  xrlelttr  13070  xnn0xaddcl  13150  fzen  13457  bernneq  14152  swrdswrdlem  14627  repsdf2  14701  limsupbnd2  15406  mulcn2  15519  prodmolem2  15858  dvdsmod0  16185  lcmfunsnlem1  16564  divgcdcoprm0  16592  maxprmfct  16636  pceu  16774  dvdsprmpweqnn  16813  oddprmdvds  16831  infpnlem1  16838  prmgaplem6  16984  imasaddfnlem  17449  initoeu1  17935  termoeu1  17942  plelttr  18265  gsumval2a  18610  cycsubm  19131  symgfix2  19345  psgnunilem4  19426  lsmmod  19604  efgrelexlemb  19679  imasabl  19805  pgpfac1lem5  20010  rngqiprngimf1lem  21249  rngqiprngimfo  21256  nzerooringczr  21435  lindfrn  21776  mat1dimcrng  22421  dmatelnd  22440  mdetunilem7  22562  cpmatacl  22660  cpmatmcllem  22662  lmss  23242  hausnei2  23297  isnrm2  23302  isnrm3  23303  cmpsublem  23343  2ndcdisj  23400  txcnpi  23552  tx1stc  23594  fgcl  23822  ufileu  23863  fmfnfmlem4  23901  fmfnfm  23902  alexsubALTlem4  23994  alexsubALT  23995  tmdgsum2  24040  prdsxmslem2  24473  ovolicc2  25479  volfiniun  25504  dyadmax  25555  ellimc3  25836  dvlip2  25956  dvne0  25972  dvfsumlem2  25989  taylthlem2  26338  zabsle1  27263  2lgslem3  27371  2sqreulem3  27420  ltlesnd  27743  cutsun12  27786  mulsproplem9  28120  mulsprop  28126  bdayons  28272  n0ssoldg  28349  eucliddivs  28372  bdayfinbndlem1  28463  axcontlem4  29040  uhgr2edg  29281  ushgredgedg  29302  ushgredgedgloop  29304  nb3grprlem1  29453  rusgr1vtx  29662  wlkonl1iedg  29737  uhgrwkspthlem2  29827  usgr2wlkneq  29829  usgr2trlncl  29833  uspgrn2crct  29881  wspthsnonn0vne  29990  usgrwwlks2on  30031  umgrwwlks2on  30032  elwspths2on  30035  elwspths2onw  30036  clwlkclwwlkf1lem3  30081  erclwwlktr  30097  erclwwlkntr  30146  frgrnbnb  30368  frgr2wwlk1  30404  frrusgrord  30416  wlkl0  30442  isch3  31316  ocin  31371  shmodsi  31464  spansneleq  31645  stj  32310  atom1d  32428  atcvat2i  32462  chirredlem1  32465  chirredi  32469  mdsymlem3  32480  mdsymlem6  32483  ssdifidlprm  33539  bnj849  35081  fineqvinfep  35281  pconnconn  35425  cvmsss2  35468  cvmliftlem7  35485  satfv0  35552  satfv0fun  35565  satffunlem  35595  satffunlem1lem1  35596  satffunlem2lem1  35598  mclsind  35764  dfon2lem9  35983  dfon2  35984  cgrextend  36202  btwntriv2  36206  btwncomim  36207  btwnexch3  36214  funtransport  36225  ifscgr  36238  colinearxfr  36269  lineext  36270  fscgr  36274  outsideoftr  36323  trer  36510  finminlem  36512  fnessref  36551  fgmin  36564  bj-andnotim  36788  bj-alanim  36812  bj-0int  37302  relowlssretop  37564  finorwe  37583  finxpsuclem  37598  wl-ax13lem1  37695  poimirlem29  37846  itg2addnclem3  37870  itg2addnc  37871  areacirc  37910  ismtybndlem  38003  heibor1lem  38006  iss2  38533  disjlem17  39054  membpartlem19  39066  prtlem17  39132  riotasvd  39212  lshpsmreu  39365  atnle  39573  cvratlem  39677  cvrat2  39685  3dim1  39723  2llnjN  39823  2lplnj  39876  linepsubN  40008  pmapsub  40024  paddasslem14  40089  pclfinN  40156  ispsubcl2N  40203  pclfinclN  40206  ldilval  40369  trlord  40825  cdlemk36  41169  dihlsscpre  41490  baerlem3lem2  41966  baerlem5alem2  41967  baerlem5blem2  41968  pellexlem5  43071  pellex  43073  pell1234qrmulcl  43093  pellfundex  43124  cantnfresb  43562  omabs2  43570  relexpmulnn  43946  clsk1indlem3  44280  19.41rg  44787  iunconnlem2  45171  relpmin  45189  or2expropbi  47276  fcoresf1  47311  euoreqb  47351  2reu8i  47355  dfatcolem  47497  f1oresf1o2  47533  nltle2tri  47555  imasetpreimafvbijlemf1  47646  iccpartnel  47680  ich2exprop  47713  ichreuopeq  47715  paireqne  47753  prprelprb  47759  reupr  47764  reuopreuprim  47768  fmtnofac2lem  47810  sfprmdvdsmersenne  47845  lighneallem3  47849  lighneallem4  47852  requad2  47865  bgoldbtbnd  48051  dfnbgr6  48099  isubgredg  48108  grimuhgr  48129  grimco  48131  uhgrimedgi  48132  isuspgrimlem  48137  clnbgrgrimlem  48175  grimedg  48177  gpgvtxedg0  48305  gpgvtxedg1  48306  gpgedg2ov  48308  gpgedg2iv  48309  pgnbgreunbgrlem1  48355  pgnbgreunbgrlem2lem1  48356  pgnbgreunbgrlem2lem2  48357  pgnbgreunbgrlem2lem3  48358  pgnbgreunbgrlem2  48359  pgnbgreunbgrlem3  48360  pgnbgreunbgrlem4  48361  pgnbgreunbgrlem5  48365  pgnbgreunbgrlem6  48366  pgnbgreunbgr  48367  upgrwlkupwlk  48382  ldepspr  48715  affinecomb1  48944  itsclc0  49013  aacllem  50042