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

Theorem 3anbi123i 1152
 Description: Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.)
Hypotheses
Ref Expression
bi3.1 (𝜑𝜓)
bi3.2 (𝜒𝜃)
bi3.3 (𝜏𝜂)
Assertion
Ref Expression
3anbi123i ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))

Proof of Theorem 3anbi123i
StepHypRef Expression
1 bi3.1 . . . 4 (𝜑𝜓)
2 bi3.2 . . . 4 (𝜒𝜃)
31, 2anbi12i 629 . . 3 ((𝜑𝜒) ↔ (𝜓𝜃))
4 bi3.3 . . 3 (𝜏𝜂)
53, 4anbi12i 629 . 2 (((𝜑𝜒) ∧ 𝜏) ↔ ((𝜓𝜃) ∧ 𝜂))
6 df-3an 1086 . 2 ((𝜑𝜒𝜏) ↔ ((𝜑𝜒) ∧ 𝜏))
7 df-3an 1086 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
85, 6, 73bitr4i 306 1 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  3anbi1i  1154  3anbi2i  1155  3anbi3i  1156  syl3anb  1158  an33rean  1480  an33reanOLD  1481  cadnot  1617  f13dfv  7010  axgroth5  10238  axgroth6  10242  cotr2g  14330  cbvprod  15264  isstruct  16491  pmtr3ncomlem1  18597  opprsubg  19386  issubgr  27071  nbgrsym  27163  nb3grpr  27182  cplgr3v  27235  usgr2pthlem  27562  umgr2adedgwlk  27741  umgrwwlks2on  27753  elwspths2spth  27763  clwwlkccat  27785  clwlkclwwlk  27797  3wlkdlem8  27962  frgr3v  28070  or3dir  30242  unelldsys  31542  bnj156  32123  bnj206  32126  bnj887  32161  bnj121  32267  bnj130  32271  bnj605  32304  bnj581  32305  brpprod3b  33476  brapply  33527  brrestrict  33538  dfrdg4  33540  brsegle  33697  dfeqvrels3  36003  tendoset  38074
 Copyright terms: Public domain W3C validator