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

Theorem 3anbi123i 1140
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 678 . . 3  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)
4 bi3.3 . . 3  |-  ( ta  <->  et )
53, 4anbi12i 678 . 2  |-  ( ( ( ph  /\  ch )  /\  ta )  <->  ( ( ps  /\  th )  /\  et ) )
6 df-3an 936 . 2  |-  ( (
ph  /\  ch  /\  ta ) 
<->  ( ( ph  /\  ch )  /\  ta )
)
7 df-3an 936 . 2  |-  ( ( ps  /\  th  /\  et )  <->  ( ( ps 
/\  th )  /\  et ) )
85, 6, 73bitr4i 268 1  |-  ( (
ph  /\  ch  /\  ta ) 
<->  ( ps  /\  th  /\  et ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3anbi1i  1142  3anbi2i  1143  3anbi3i  1144  syl3anb  1225  cadnot  1385  axgroth5  8491  axgroth6  8495  isstruct  13205  opprsubg  15467  cbvprod  24418  brpprod3b  24812  brapply  24862  brrestrict  24873  dfrdg4  24874  brsegle  25117  nb3grapr  27399  cusgra3v  27409  frgra3v  27594  bnj156  28267  bnj206  28270  bnj887  28306  bnj121  28413  bnj130  28417  bnj605  28450  bnj581  28451  tendoset  30766
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator