MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anbi23d Structured version   Visualization version   GIF version

Theorem 3anbi23d 1436
Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
Hypotheses
Ref Expression
3anbi12d.1 (𝜑 → (𝜓𝜒))
3anbi12d.2 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
3anbi23d (𝜑 → ((𝜂𝜓𝜃) ↔ (𝜂𝜒𝜏)))

Proof of Theorem 3anbi23d
StepHypRef Expression
1 biidd 265 . 2 (𝜑 → (𝜂𝜂))
2 3anbi12d.1 . 2 (𝜑 → (𝜓𝜒))
3 3anbi12d.2 . 2 (𝜑 → (𝜃𝜏))
41, 2, 33anbi123d 1433 1 (𝜑 → ((𝜂𝜓𝜃) ↔ (𝜂𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  opeq2  4768  f1dom3el3dif  7009  wrecseq123  7935  oeeui  8215  fpwwe2lem5  10049  pwfseqlem4a  10076  pwfseqlem4  10077  pfxccatin12lem3  14089  prodeq2w  15261  prodeq2ii  15262  divalg  15747  dfgcd2  15887  iscatd2  16947  posi  17555  issubg3  18292  pmtrfrn  18581  psgnunilem2  18618  psgnunilem3  18619  lmhmpropd  19841  lbsacsbs  19924  frlmphl  20473  neiptoptop  21739  neiptopnei  21740  cnhaus  21962  nrmsep  21965  dishaus  21990  ordthauslem  21991  nconnsubb  22031  pthaus  22246  txhaus  22255  xkohaus  22261  regr1lem  22347  isust  22812  ustuqtop4  22853  methaus  23130  metnrmlem3  23469  iscau4  23886  pmltpclem1  24055  dvfsumlem2  24633  aannenlem1  24927  aannenlem2  24928  istrkgcb  26253  hlbtwn  26408  iscgra  26606  dfcgra2  26627  f1otrge  26669  axlowdim  26758  axeuclidlem  26759  eengtrkg  26783  clwwlk  27771  upgr3v3e3cycl  27968  upgr4cycl4dv4e  27973  numclwwlk5  28176  ex-opab  28220  l2p  28265  vciOLD  28347  isvclem  28363  isnvlem  28396  dipass  28631  adj1  29719  adjeq  29721  cnlnssadj  29866  br8d  30377  carsgmon  31680  carsgsigalem  31681  carsgclctunlem2  31685  carsgclctun  31687  bnj1154  32379  br8  33100  br6  33101  br4  33102  frecseq123  33227  brsslt  33362  fvtransport  33601  brcgr3  33615  brfs  33648  fscgr  33649  btwnconn1lem11  33666  brsegle  33677  fvray  33710  linedegen  33712  fvline  33713  bj-isclm  34700  poimirlem28  35078  poimirlem32  35082  heiborlem2  35243  hlsuprexch  36670  3dim1lem5  36755  lplni2  36826  2llnjN  36856  lvoli2  36870  2lplnj  36909  cdleme18d  37584  cdlemg1cex  37877  ismrc  39629  monotoddzzfi  39870  oddcomabszz  39872  zindbi  39874  rmydioph  39942  fsumiunss  42204  sumnnodd  42259  stoweidlem31  42660  stoweidlem34  42663  stoweidlem43  42672  stoweidlem48  42677  fourierdlem42  42778  sge0iunmptlemre  43041  sge0iunmpt  43044  vonioo  43308  vonicc  43311  fundcmpsurinjpreimafv  43912
  Copyright terms: Public domain W3C validator