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

Theorem 3anbi1i 1142
Description: Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
Hypothesis
Ref Expression
3anbi1i.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
3anbi1i  |-  ( (
ph  /\  ch  /\  th ) 
<->  ( ps  /\  ch  /\ 
th ) )

Proof of Theorem 3anbi1i
StepHypRef Expression
1 3anbi1i.1 . 2  |-  ( ph  <->  ps )
2 biid 227 . 2  |-  ( ch  <->  ch )
3 biid 227 . 2  |-  ( th  <->  th )
41, 2, 33anbi123i 1140 1  |-  ( (
ph  /\  ch  /\  th ) 
<->  ( ps  /\  ch  /\ 
th ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ w3a 934
This theorem is referenced by:  iinfi  7171  fzolb  10880  sqrlem5  11732  bitsmod  12627  isfunc  13738  istps5OLD  16662  txcn  17320  trfil2  17582  or3dir  23124  bnj976  28809  bnj543  28925  bnj594  28944  bnj917  28966  dath  29925  cdleme0moN  30414
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