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

Theorem 3anbi3i 1181
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 236 . 2  |-  ( ch  <->  ch )
2 biid 236 . 2  |-  ( th  <->  th )
3 3anbi1i.1 . 2  |-  ( ph  <->  ps )
41, 2, 33anbi123i 1177 1  |-  ( ( ch  /\  th  /\  ph )  <->  ( ch  /\  th 
/\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  dfer2  7205  axgroth2  9096  oppgsubm  15988  xrsdsreclb  17978  ordthaus  19113  qtopeu  19414  regr1lem2  19438  isfbas2  19533  nbgrasym  23493  xrge0adddir  26293  dfon2lem7  27739  outsideofcom  28296  linecom  28318  linerflx2  28319  dmatsubcl  31034  bnj964  32239  bnj1033  32263  ishlat2  33307  lhpex2leN  33966
  Copyright terms: Public domain W3C validator