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  10858  imasdsval  13418  iscatd2  13583  ispos  14081  rngpropd  15372  dvfsumlem2  19374  lt2addrd  23249  xlt2addrd  23253  sigaval  23471  issgon  23484  dfrtrcl2  24045  axlowdim  24589  axeuclid  24591  brofs  24628  funtransport  24654  fvtransport  24655  brifs  24666  ifscgr  24667  brcgr3  24669  cgr3permute3  24670  brfs  24702  btwnconn1lem11  24720  funray  24763  fvray  24764  funline  24765  fvline  24767  isded  25736  dedi  25737  ismonb2  25812  isepib2  25822  morcatset1  25915  domcatfun  25925  codcatfun  25934  isrocatset  25957  isibg2  26110  isibg2aa  26112  isibg2aalem1  26113  rmydioph  27107  psgnunilem1  27416  lpolsetN  31672
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