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

Theorem 3anbi1i 1144
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 228 . 2  |-  ( ch  <->  ch )
3 biid 228 . 2  |-  ( th  <->  th )
41, 2, 33anbi123i 1142 1  |-  ( (
ph  /\  ch  /\  th ) 
<->  ( ps  /\  ch  /\ 
th ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ w3a 936
This theorem is referenced by:  iinfi  7358  fzolb  11076  sqrlem5  11980  bitsmod  12876  isfunc  13989  istps5OLD  16913  txcn  17580  trfil2  17841  bnj976  28487  bnj543  28603  bnj594  28622  bnj917  28644  dath  29851
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