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

Theorem 3anbi3i 1184
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 1180 1  |-  ( ( ch  /\  th  /\  ph )  <->  ( ch  /\  th 
/\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ w3a 968
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 970
This theorem is referenced by:  dfer2  7302  axgroth2  9192  oppgsubm  16185  xrsdsreclb  18226  ordthaus  19644  qtopeu  19945  regr1lem2  19969  isfbas2  20064  nbgrasym  24101  xrge0adddir  27194  dfon2lem7  28648  outsideofcom  29205  linecom  29227  linerflx2  29228  fourierdlem103  31329  fourierdlem104  31330  bnj964  32955  bnj1033  32979  ishlat2  34025  lhpex2leN  34684
  Copyright terms: Public domain W3C validator