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

Theorem 3anbi123i 1270
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 733 . . 3 ((𝜑𝜒) ↔ (𝜓𝜃))
4 bi3.3 . . 3 (𝜏𝜂)
53, 4anbi12i 733 . 2 (((𝜑𝜒) ∧ 𝜏) ↔ ((𝜓𝜃) ∧ 𝜂))
6 df-3an 1056 . 2 ((𝜑𝜒𝜏) ↔ ((𝜑𝜒) ∧ 𝜏))
7 df-3an 1056 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
85, 6, 73bitr4i 292 1 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  w3a 1054
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 1056
This theorem is referenced by:  3anbi1i  1272  3anbi2i  1273  3anbi3i  1274  syl3anb  1409  an33rean  1486  cadnot  1594  f13dfv  6570  axgroth5  9684  axgroth6  9688  cotr2g  13761  cbvprod  14689  isstruct  15917  pmtr3ncomlem1  17939  opprsubg  18682  issubgr  26208  nbgrsym  26308  nbgrsymOLD  26309  nb3grpr  26328  cplgr3v  26387  usgr2pthlem  26715  umgr2adedgwlk  26910  umgrwwlks2on  26923  elwspths2spth  26934  clwlkclwwlk  26968  clwlksfclwwlk  27049  3wlkdlem8  27145  frgr3v  27255  clwwlkccat  27332  or3dir  29436  unelldsys  30349  bnj156  30922  bnj206  30925  bnj887  30961  bnj121  31066  bnj130  31070  bnj605  31103  bnj581  31104  brpprod3b  32119  brapply  32170  brrestrict  32181  dfrdg4  32183  brsegle  32340  tendoset  36364
  Copyright terms: Public domain W3C validator