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

Theorem 3anbi3i 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
3anbi3i  |-  ( ( ch  /\  th  /\  ph )  <->  ( ch  /\  th 
/\  ps ) )

Proof of Theorem 3anbi3i
StepHypRef Expression
1 biid 227 . 2  |-  ( ch  <->  ch )
2 biid 227 . 2  |-  ( th  <->  th )
3 3anbi1i.1 . 2  |-  ( ph  <->  ps )
41, 2, 33anbi123i 1140 1  |-  ( ( ch  /\  th  /\  ph )  <->  ( ch  /\  th 
/\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ w3a 934
This theorem is referenced by:  dfer2  6661  axgroth2  8447  oppgsubm  14835  xrsdsreclb  16418  ordthaus  17112  qtopeu  17407  regr1lem2  17431  isfbas2  17530  or3dir  23124  xrge0adddir  23332  dfon2lem7  24145  outsideofcom  24751  linecom  24773  linerflx2  24774  vecax3  25455  nbgrasym  28152  bnj964  28975  bnj1033  28999  ishlat2  29543  lhpex2leN  30202
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