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

Theorem 3anbi3i 1146
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 228 . 2  |-  ( ch  <->  ch )
2 biid 228 . 2  |-  ( th  <->  th )
3 3anbi1i.1 . 2  |-  ( ph  <->  ps )
41, 2, 33anbi123i 1142 1  |-  ( ( ch  /\  th  /\  ph )  <->  ( ch  /\  th 
/\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ w3a 936
This theorem is referenced by:  dfer2  6906  axgroth2  8700  oppgsubm  15158  xrsdsreclb  16745  ordthaus  17448  qtopeu  17748  regr1lem2  17772  isfbas2  17867  nbgrasym  21449  xrge0adddir  24215  dfon2lem7  25416  outsideofcom  26062  linecom  26084  linerflx2  26085  bnj964  29314  bnj1033  29338  ishlat2  30151  lhpex2leN  30810
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator