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 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 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 369    /\ 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 371  df-3an 976
This theorem is referenced by:  3anbi1i  1188  3anbi2i  1189  3anbi3i  1190  syl3anb  1272  an33rean  1343  cadnot  1449  f13dfv  6165  axgroth5  9205  axgroth6  9209  cbvprod  13704  isstruct  14624  pmtr3ncomlem1  16477  opprsubg  17264  nb3grapr  24431  cusgra3v  24442  wwlknfi  24716  frgra3v  24980  or3dir  27346  brpprod3b  29513  brapply  29564  brrestrict  29575  dfrdg4  29576  brsegle  29734  usgra2pthlem1  32307  bnj156  33651  bnj206  33654  bnj887  33691  bnj121  33796  bnj130  33800  bnj605  33833  bnj581  33834  tendoset  36360  cotr2g  37614
  Copyright terms: Public domain W3C validator