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

Theorem 3anbi1i 1198
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 240 . 2  |-  ( ch  <->  ch )
3 biid 240 . 2  |-  ( th  <->  th )
41, 2, 33anbi123i 1196 1  |-  ( (
ph  /\  ch  /\  th ) 
<->  ( ps  /\  ch  /\ 
th ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    /\ w3a 984
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189  df-an 373  df-3an 986
This theorem is referenced by:  iinfi  7928  fzolb  11923  brfi1uzind  12648  opfi1uzind  12651  sqrlem5  13303  bitsmod  14403  isfunc  15762  txcn  20634  trfil2  20895  eulerpartlemn  29207  bnj976  29582  bnj543  29697  bnj594  29716  bnj917  29738  topdifinffinlem  31743  dath  33295  elfzolborelfzop1  40303  nnolog2flm1  40388
  Copyright terms: Public domain W3C validator