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

Theorem 3anbi123i 1143
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 680 . . 3  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)
4 bi3.3 . . 3  |-  ( ta  <->  et )
53, 4anbi12i 680 . 2  |-  ( ( ( ph  /\  ch )  /\  ta )  <->  ( ( ps  /\  th )  /\  et ) )
6 df-3an 939 . 2  |-  ( (
ph  /\  ch  /\  ta ) 
<->  ( ( ph  /\  ch )  /\  ta )
)
7 df-3an 939 . 2  |-  ( ( ps  /\  th  /\  et )  <->  ( ( ps 
/\  th )  /\  et ) )
85, 6, 73bitr4i 270 1  |-  ( (
ph  /\  ch  /\  ta ) 
<->  ( ps  /\  th  /\  et ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    /\ w3a 937
This theorem is referenced by:  3anbi1i  1145  3anbi2i  1146  3anbi3i  1147  syl3anb  1228  cadnot  1404  axgroth5  8701  axgroth6  8705  isstruct  13481  opprsubg  15743  nb3grapr  21464  cusgra3v  21475  or3dir  23954  cbvprod  25243  brpprod3b  25734  brapply  25785  brrestrict  25796  dfrdg4  25797  brsegle  26044  f13dfv  28087  usgra2pthlem1  28336  frgra3v  28454  bnj156  29157  bnj206  29160  bnj887  29196  bnj121  29303  bnj130  29307  bnj605  29340  bnj581  29341  tendoset  31618
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator