MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anbi13d Structured version   Unicode version

Theorem 3anbi13d 1256
Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
Hypotheses
Ref Expression
3anbi12d.1  |-  ( ph  ->  ( ps  <->  ch )
)
3anbi12d.2  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
3anbi13d  |-  ( ph  ->  ( ( ps  /\  et  /\  th )  <->  ( ch  /\  et  /\  ta )
) )

Proof of Theorem 3anbi13d
StepHypRef Expression
1 3anbi12d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 biidd 229 . 2  |-  ( ph  ->  ( et  <->  et )
)
3 3anbi12d.2 . 2  |-  ( ph  ->  ( th  <->  ta )
)
41, 2, 33anbi123d 1254 1  |-  ( ph  ->  ( ( ps  /\  et  /\  th )  <->  ( ch  /\  et  /\  ta )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936
This theorem is referenced by:  3anbi3d  1260  ax11wdemo  1738  cofsmo  8139  axdc3lem3  8322  axdc3lem4  8323  iscatd2  13896  opprsubrg  15879  lsspropd  16083  lmres  17354  cnhaus  17408  regsep2  17430  dishaus  17436  ordthauslem  17437  nconsubb  17476  pthaus  17660  txhaus  17669  xkohaus  17675  regr1lem  17761  ustval  18222  methaus  18540  metnrmlem3  18881  pmltpclem1  19335  ex-opab  21730  isnvlem  22079  ajval  22353  adjeu  23382  adjval  23383  adj1  23426  adjeq  23428  cnlnssadj  23573  lt2addrd  24105  xlt2addrd  24114  measval  24542  br8  25369  br6  25370  br4  25371  wfrlem1  25523  wfrlem15  25537  nofulllem5  25626  axeuclidlem  25866  brcgr3  25945  brsegle  26007  fvray  26040  linedegen  26042  fvline  26043  zindbi  26963  jm2.27  27033  psgnunilem1  27348  stoweidlem43  27723  2wlkonot  28249  2spthonot  28250  usg2spthonot0  28273  vdn0frgrav2  28315  vdgn0frgrav2  28316  vdn1frgrav2  28317  vdgn1frgrav2  28318  isopos  29879  hlsuprexch  30079  2llnjN  30265  2lplnj  30318  cdlemk42  31639
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator