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  6677  axgroth2  8463  oppgsubm  14851  xrsdsreclb  16434  ordthaus  17128  qtopeu  17423  regr1lem2  17447  isfbas2  17546  or3dir  23140  xrge0adddir  23347  dfon2lem7  24216  outsideofcom  24823  linecom  24845  linerflx2  24846  vecax3  25558  nbgrasym  28286  bnj964  29291  bnj1033  29315  ishlat2  30165  lhpex2leN  30824
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