MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anbi1i Structured version   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  7414  fzolb  11135  sqrlem5  12042  bitsmod  12938  isfunc  14051  istps5OLD  16979  txcn  17648  trfil2  17909  bnj976  29049  bnj543  29165  bnj594  29184  bnj917  29206  dath  30434
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