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

Theorem 3anbi123i 1159
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 735 . . 3 ((𝜑𝜒) ↔ (𝜓𝜃))
4 bi3.3 . . 3 (𝜏𝜂)
53, 4anbi12i 735 . 2 (((𝜑𝜒) ∧ 𝜏) ↔ ((𝜓𝜃) ∧ 𝜂))
6 df-3an 1074 . 2 ((𝜑𝜒𝜏) ↔ ((𝜑𝜒) ∧ 𝜏))
7 df-3an 1074 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
85, 6, 73bitr4i 292 1 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  3anbi1i  1161  3anbi2i  1162  3anbi3i  1163  syl3anb  1165  an33rean  1595  cadnot  1703  f13dfv  6693  axgroth5  9838  axgroth6  9842  cotr2g  13916  cbvprod  14844  isstruct  16072  pmtr3ncomlem1  18093  opprsubg  18836  issubgr  26362  nbgrsym  26462  nbgrsymOLD  26463  nb3grpr  26482  cplgr3v  26541  usgr2pthlem  26869  umgr2adedgwlk  27065  umgrwwlks2on  27078  elwspths2spth  27089  clwwlkccat  27113  clwlkclwwlk  27125  clwlksfclwwlkOLD  27216  3wlkdlem8  27319  frgr3v  27429  or3dir  29617  unelldsys  30530  bnj156  31103  bnj206  31106  bnj887  31142  bnj121  31247  bnj130  31251  bnj605  31284  bnj581  31285  brpprod3b  32300  brapply  32351  brrestrict  32362  dfrdg4  32364  brsegle  32521  tendoset  36549
  Copyright terms: Public domain W3C validator