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

Theorem 3anbi3i 1188
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 1184 1  |-  ( ( ch  /\  th  /\  ph )  <->  ( ch  /\  th 
/\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ w3a 972
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 974
This theorem is referenced by:  dfer2  7310  axgroth2  9201  oppgsubm  16266  xrsdsreclb  18333  ordthaus  19751  qtopeu  20083  regr1lem2  20107  isfbas2  20202  nbgrasym  24304  xrge0adddir  27548  dfon2lem7  29189  outsideofcom  29746  linecom  29768  linerflx2  29769  fourierdlem103  31877  fourierdlem104  31878  bnj964  33708  bnj1033  33732  ishlat2  34780  lhpex2leN  35439
  Copyright terms: Public domain W3C validator