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

Theorem 3anbi123i 1185
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 975 . 2  |-  ( (
ph  /\  ch  /\  ta ) 
<->  ( ( ph  /\  ch )  /\  ta )
)
7 df-3an 975 . 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 973
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 975
This theorem is referenced by:  3anbi1i  1187  3anbi2i  1188  3anbi3i  1189  syl3anb  1271  an33rean  1342  cadnot  1446  f13dfv  6167  axgroth5  9201  axgroth6  9205  isstruct  14499  pmtr3ncomlem1  16301  opprsubg  17081  nb3grapr  24145  cusgra3v  24156  wwlknfi  24430  frgra3v  24694  or3dir  27060  cbvprod  28640  brpprod3b  29130  brapply  29181  brrestrict  29192  dfrdg4  29193  brsegle  29351  usgra2pthlem1  31836  bnj156  32872  bnj206  32875  bnj887  32911  bnj121  33016  bnj130  33020  bnj605  33053  bnj581  33054  tendoset  35564
  Copyright terms: Public domain W3C validator