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

Theorem 3anbi12d 1253
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
3anbi12d  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  <->  ( ch  /\ 
ta  /\  et )
) )

Proof of Theorem 3anbi12d
StepHypRef Expression
1 3anbi12d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 3anbi12d.2 . 2  |-  ( ph  ->  ( th  <->  ta )
)
3 biidd 228 . 2  |-  ( ph  ->  ( et  <->  et )
)
41, 2, 33anbi123d 1252 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  <->  ( ch  /\ 
ta  /\  et )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  3anbi1d  1256  3anbi2d  1257  fseq1m1p1  10874  imasdsval  13434  iscatd2  13599  ispos  14097  rngpropd  15388  dvfsumlem2  19390  lt2addrd  23264  xlt2addrd  23268  sigaval  23486  issgon  23499  dfrtrcl2  24060  axlowdim  24661  axeuclid  24663  brofs  24700  funtransport  24726  fvtransport  24727  brifs  24738  ifscgr  24739  brcgr3  24741  cgr3permute3  24742  brfs  24774  btwnconn1lem11  24792  funray  24835  fvray  24836  funline  24837  fvline  24839  isded  25839  dedi  25840  ismonb2  25915  isepib2  25925  morcatset1  26018  domcatfun  26028  codcatfun  26037  isrocatset  26060  isibg2  26213  isibg2aa  26215  isibg2aalem1  26216  rmydioph  27210  psgnunilem1  27519  lpolsetN  32294
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator