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

Theorem 3anbi123i 1219
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 711 . . 3  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)
4 bi3.3 . . 3  |-  ( ta  <->  et )
53, 4anbi12i 711 . 2  |-  ( ( ( ph  /\  ch )  /\  ta )  <->  ( ( ps  /\  th )  /\  et ) )
6 df-3an 1009 . 2  |-  ( (
ph  /\  ch  /\  ta ) 
<->  ( ( ph  /\  ch )  /\  ta )
)
7 df-3an 1009 . 2  |-  ( ( ps  /\  th  /\  et )  <->  ( ( ps 
/\  th )  /\  et ) )
85, 6, 73bitr4i 285 1  |-  ( (
ph  /\  ch  /\  ta ) 
<->  ( ps  /\  th  /\  et ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  3anbi1i  1221  3anbi2i  1222  3anbi3i  1223  syl3anb  1335  an33rean  1411  cadnot  1526  f13dfv  6191  axgroth5  9267  axgroth6  9271  cotr2g  13115  cbvprod  14046  isstruct  15209  pmtr3ncomlem1  17192  opprsubg  17942  nb3grapr  25260  cusgra3v  25271  wwlknfi  25545  frgra3v  25809  or3dir  28183  unelldsys  29054  bnj156  29608  bnj206  29611  bnj887  29648  bnj121  29753  bnj130  29757  bnj605  29790  bnj581  29791  brpprod3b  30725  brapply  30776  brrestrict  30787  dfrdg4  30789  brsegle  30946  tendoset  34397  issubgr  39507  nbgrsym  39601  nb3grpr  39620  umgr2adedgwlk  40067  31wlkdlem8  40081  usgra2pthlem1  40175
  Copyright terms: Public domain W3C validator