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

Theorem 3anbi123i 1176
Description: Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.)
Hypotheses
Ref Expression
bi3.1  |-  ( ph  <->  ps )
bi3.2  |-  ( ch  <->  th )
bi3.3  |-  ( ta  <->  et )
Assertion
Ref Expression
3anbi123i  |-  ( (
ph  /\  ch  /\  ta ) 
<->  ( ps  /\  th  /\  et ) )

Proof of Theorem 3anbi123i
StepHypRef Expression
1 bi3.1 . . . 4  |-  ( ph  <->  ps )
2 bi3.2 . . . 4  |-  ( ch  <->  th )
31, 2anbi12i 697 . . 3  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)
4 bi3.3 . . 3  |-  ( ta  <->  et )
53, 4anbi12i 697 . 2  |-  ( ( ( ph  /\  ch )  /\  ta )  <->  ( ( ps  /\  th )  /\  et ) )
6 df-3an 967 . 2  |-  ( (
ph  /\  ch  /\  ta ) 
<->  ( ( ph  /\  ch )  /\  ta )
)
7 df-3an 967 . 2  |-  ( ( ps  /\  th  /\  et )  <->  ( ( ps 
/\  th )  /\  et ) )
85, 6, 73bitr4i 277 1  |-  ( (
ph  /\  ch  /\  ta ) 
<->  ( ps  /\  th  /\  et ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    /\ 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:  3anbi1i  1178  3anbi2i  1179  3anbi3i  1180  syl3anb  1261  an33rean  1332  cadnot  1436  axgroth5  8991  axgroth6  8995  isstruct  14184  pmtr3ncomlem1  15979  opprsubg  16728  nb3grapr  23361  cusgra3v  23372  or3dir  25853  cbvprod  27428  brpprod3b  27918  brapply  27969  brrestrict  27980  dfrdg4  27981  brsegle  28139  f13dfv  30147  usgra2pthlem1  30300  wwlknfi  30370  frgra3v  30594  bnj156  31719  bnj206  31722  bnj887  31758  bnj121  31863  bnj130  31867  bnj605  31900  bnj581  31901  tendoset  34403
  Copyright terms: Public domain W3C validator