MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anbi3i 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  6892  axgroth2  8684  oppgsubm  15141  xrsdsreclb  16728  ordthaus  17431  qtopeu  17731  regr1lem2  17755  isfbas2  17850  nbgrasym  21432  xrge0adddir  24198  dfon2lem7  25395  outsideofcom  26005  linecom  26027  linerflx2  26028  bnj964  29066  bnj1033  29090  ishlat2  29882  lhpex2leN  30541
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