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 261 . 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 205  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 206  df-an 395  df-3an 1086
This theorem is referenced by:  f1dom3el3dif  7284  xpord2lem  8156  xpord3lem  8163  frecseq123  8297  wrecseq123OLD  8330  oeeui  8632  sbthfi  9236  fpwwe2lem4  10677  pwfseqlem4a  10704  pwfseqlem4  10705  pfxccatin12lem3  14740  prodeq2w  15914  prodeq2ii  15915  divalg  16405  dfgcd2  16547  iscatd2  17694  posi  18342  issubg3  19138  pmtrfrn  19456  psgnunilem2  19493  psgnunilem3  19494  lmhmpropd  21051  lbsacsbs  21137  frlmphl  21779  neiptoptop  23126  neiptopnei  23127  cnhaus  23349  nrmsep  23352  dishaus  23377  ordthauslem  23378  nconnsubb  23418  pthaus  23633  txhaus  23642  xkohaus  23648  regr1lem  23734  isust  24199  ustuqtop4  24240  methaus  24520  metnrmlem3  24868  iscau4  25298  pmltpclem1  25468  dvfsumlem2  26052  dvfsumlem2OLD  26053  aannenlem1  26356  aannenlem2  26357  brsslt  27815  istrkgcb  28383  hlbtwn  28538  iscgra  28736  dfcgra2  28757  f1otrge  28799  axlowdim  28895  axeuclidlem  28896  eengtrkg  28920  clwwlk  29916  upgr3v3e3cycl  30113  upgr4cycl4dv4e  30118  numclwwlk5  30321  ex-opab  30365  l2p  30412  vciOLD  30494  isvclem  30510  isnvlem  30543  dipass  30778  adj1  31866  adjeq  31868  cnlnssadj  32013  br8d  32530  dvdsruasso2  33261  dfufd2lem  33424  constrsuc  33596  constrconj  33603  carsgmon  34148  carsgsigalem  34149  carsgclctunlem2  34153  carsgclctun  34155  bnj1154  34844  br8  35578  br6  35579  br4  35580  fvtransport  35856  brcgr3  35870  brfs  35903  fscgr  35904  btwnconn1lem11  35921  brsegle  35932  fvray  35965  linedegen  35967  fvline  35968  bj-isclm  36998  poimirlem28  37349  poimirlem32  37353  heiborlem2  37513  hlsuprexch  39080  3dim1lem5  39165  lplni2  39236  2llnjN  39266  lvoli2  39280  2lplnj  39319  cdleme18d  39994  cdlemg1cex  40287  ismrc  42358  monotoddzzfi  42600  oddcomabszz  42602  zindbi  42604  rmydioph  42672  nnoeomeqom  42978  rp-brsslt  43090  fsumiunss  45196  sumnnodd  45251  stoweidlem31  45652  stoweidlem34  45655  stoweidlem43  45664  stoweidlem48  45669  fourierdlem42  45770  sge0iunmptlemre  46036  sge0iunmpt  46039  vonioo  46303  vonicc  46306  fundcmpsurinjpreimafv  46980  sepfsepc  48261  iscnrm3rlem8  48281  iscnrm3llem2  48284
  Copyright terms: Public domain W3C validator