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

Theorem 3anbi123i 1186
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 695 . . 3  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)
4 bi3.3 . . 3  |-  ( ta  <->  et )
53, 4anbi12i 695 . 2  |-  ( ( ( ph  /\  ch )  /\  ta )  <->  ( ( ps  /\  th )  /\  et ) )
6 df-3an 976 . 2  |-  ( (
ph  /\  ch  /\  ta ) 
<->  ( ( ph  /\  ch )  /\  ta )
)
7 df-3an 976 . 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 367    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  3anbi1i  1188  3anbi2i  1189  3anbi3i  1190  syl3anb  1273  an33rean  1344  cadnot  1477  cadnotOLD  1478  f13dfv  6160  axgroth5  9231  axgroth6  9235  cotr2g  12957  cbvprod  13872  isstruct  14849  pmtr3ncomlem1  16820  opprsubg  17603  nb3grapr  24857  cusgra3v  24868  wwlknfi  25142  frgra3v  25406  or3dir  27767  unelldsys  28592  bnj156  29097  bnj206  29100  bnj887  29137  bnj121  29242  bnj130  29246  bnj605  29279  bnj581  29280  brpprod3b  30212  brapply  30263  brrestrict  30274  dfrdg4  30276  brsegle  30433  tendoset  33758  usgra2pthlem1  37963
  Copyright terms: Public domain W3C validator