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  7187  fzolb  10896  sqrlem5  11748  bitsmod  12643  isfunc  13754  istps5OLD  16678  txcn  17336  trfil2  17598  or3dir  23140  bnj976  29125  bnj543  29241  bnj594  29260  bnj917  29282  dath  30547  cdleme0moN  31036
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