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

Theorem 3anbi3i 1180
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 1176 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  7094  axgroth2  8984  oppgsubm  15868  xrsdsreclb  17835  ordthaus  18963  qtopeu  19264  regr1lem2  19288  isfbas2  19383  nbgrasym  23299  xrge0adddir  26106  dfon2lem7  27553  outsideofcom  28110  linecom  28132  linerflx2  28133  dmatsubcl  30800  bnj964  31823  bnj1033  31847  ishlat2  32838  lhpex2leN  33497
  Copyright terms: Public domain W3C validator