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  1120  ax13lem1  2374  equs5  2460  rsp2  3136  moi  3648  reu6  3656  sbciegft  3749  ss2abdv  3993  elpwunsn  4616  opthpr  4779  preqsnd  4786  opthprneg  4792  3elpr2eq  4835  invdisj  5054  snopeqop  5414  solin  5519  sotr2  5526  wefrc  5574  relop  5748  elinxp  5918  reuop  6185  dfpo2  6188  tz7.7  6277  ordtr2  6295  funopsn  7002  tpres  7058  funfvima  7088  isomin  7188  sorpsscmpl  7565  peano5  7714  peano5OLD  7715  f1oweALT  7788  poxp  7940  soxp  7941  tfr3  8201  tz7.48-1  8244  omordi  8359  odi  8372  omass  8373  oen0  8379  nndi  8416  nnmass  8417  nnmordi  8424  eroveu  8559  ssfi  8918  findcard3  8987  fiint  9021  suplub  9149  hartogs  9233  card2on  9243  unxpwdom2  9277  inf3lem2  9317  epfrs  9420  tcel  9434  frr3g  9445  dfac2b  9817  infpssr  9995  isf32lem9  10048  axdc3lem4  10140  axcclem  10144  zorn2lem7  10189  ttukeylem6  10201  brdom6disj  10219  ondomon  10250  inar1  10462  gruen  10499  indpi  10594  nqereu  10616  genpn0  10690  distrlem1pr  10712  distrlem5pr  10714  ltexprlem1  10723  reclem4pr  10737  addsrmo  10760  mulsrmo  10761  supsrlem  10798  lelttr  10996  ltlen  11006  mulgt1  11764  fzind  12348  xrlelttr  12819  xnn0xaddcl  12898  fzen  13202  bernneq  13872  swrdswrdlem  14345  repsdf2  14419  limsupbnd2  15120  mulcn2  15233  prodmolem2  15573  dvdsmod0  15897  lcmfunsnlem1  16270  divgcdcoprm0  16298  maxprmfct  16342  pceu  16475  dvdsprmpweqnn  16514  oddprmdvds  16532  infpnlem1  16539  prmgaplem6  16685  imasaddfnlem  17156  initoeu1  17642  termoeu1  17649  plelttr  17977  gsumval2a  18284  cycsubm  18736  symgfix2  18939  psgnunilem4  19020  lsmmod  19196  efgrelexlemb  19271  pgpfac1lem5  19597  lindfrn  20938  mat1dimcrng  21534  dmatelnd  21553  mdetunilem7  21675  cpmatacl  21773  cpmatmcllem  21775  lmss  22357  hausnei2  22412  isnrm2  22417  isnrm3  22418  cmpsublem  22458  2ndcdisj  22515  txcnpi  22667  tx1stc  22709  fgcl  22937  ufileu  22978  fmfnfmlem4  23016  fmfnfm  23017  alexsubALTlem4  23109  alexsubALT  23110  tmdgsum2  23155  prdsxmslem2  23591  ovolicc2  24591  volfiniun  24616  dyadmax  24667  ellimc3  24948  dvlip2  25064  dvne0  25080  zabsle1  26349  2lgslem3  26457  2sqreulem3  26506  axcontlem4  27238  uhgr2edg  27478  ushgredgedg  27499  ushgredgedgloop  27501  nb3grprlem1  27650  rusgr1vtx  27858  wlkonl1iedg  27935  uhgrwkspthlem2  28023  usgr2wlkneq  28025  usgr2trlncl  28029  uspgrn2crct  28074  wspthsnonn0vne  28183  umgrwwlks2on  28223  elwspths2on  28226  clwlkclwwlkf1lem3  28271  erclwwlktr  28287  erclwwlkntr  28336  frgrnbnb  28558  frgr2wwlk1  28594  frrusgrord  28606  wlkl0  28632  isch3  29504  ocin  29559  shmodsi  29652  spansneleq  29833  stj  30498  atom1d  30616  atcvat2i  30650  chirredlem1  30653  chirredi  30657  mdsymlem3  30668  mdsymlem6  30671  bnj849  32805  pconnconn  33093  cvmsss2  33136  cvmliftlem7  33153  satfv0  33220  satfv0fun  33233  satffunlem  33263  satffunlem1lem1  33264  satffunlem2lem1  33266  mclsind  33432  dfon2lem9  33673  dfon2  33674  ttrclselem2  33712  scutun12  33931  cgrextend  34237  btwntriv2  34241  btwncomim  34242  btwnexch3  34249  funtransport  34260  ifscgr  34273  colinearxfr  34304  lineext  34305  fscgr  34309  outsideoftr  34358  trer  34432  finminlem  34434  fnessref  34473  fgmin  34486  bj-andnotim  34697  bj-alanim  34721  bj-0int  35199  relowlssretop  35461  finorwe  35480  finxpsuclem  35495  wl-ax13lem1  35592  poimirlem29  35733  itg2addnclem3  35757  itg2addnc  35758  areacirc  35797  ismtybndlem  35891  heibor1lem  35894  iss2  36406  prtlem17  36817  riotasvd  36897  lshpsmreu  37050  atnle  37258  cvratlem  37362  cvrat2  37370  3dim1  37408  2llnjN  37508  2lplnj  37561  linepsubN  37693  pmapsub  37709  paddasslem14  37774  pclfinN  37841  ispsubcl2N  37888  pclfinclN  37891  ldilval  38054  trlord  38510  cdlemk36  38854  dihlsscpre  39175  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  pellexlem5  40571  pellex  40573  pell1234qrmulcl  40593  pellfundex  40624  relexpmulnn  41206  clsk1indlem3  41542  19.41rg  42059  iunconnlem2  42444  or2expropbi  44415  fcoresf1  44450  euoreqb  44488  2reu8i  44492  dfatcolem  44634  f1oresf1o2  44670  nltle2tri  44693  imasetpreimafvbijlemf1  44744  iccpartnel  44778  ich2exprop  44811  ichreuopeq  44813  paireqne  44851  prprelprb  44857  reupr  44862  reuopreuprim  44866  fmtnofac2lem  44908  sfprmdvdsmersenne  44943  lighneallem3  44947  lighneallem4  44950  requad2  44963  bgoldbtbnd  45149  isomuspgrlem2d  45171  isomgrsym  45176  isomgrtr  45179  upgrwlkupwlk  45190  nzerooringczr  45518  ldepspr  45702  affinecomb1  45936  itsclc0  46005  aacllem  46391