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

Theorem 3anbi123i 1156
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 628 . . 3 ((𝜑𝜒) ↔ (𝜓𝜃))
4 bi3.3 . . 3 (𝜏𝜂)
53, 4anbi12i 628 . 2 (((𝜑𝜒) ∧ 𝜏) ↔ ((𝜓𝜃) ∧ 𝜂))
6 df-3an 1089 . 2 ((𝜑𝜒𝜏) ↔ ((𝜑𝜒) ∧ 𝜏))
7 df-3an 1089 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
85, 6, 73bitr4i 303 1 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  3anbi1i  1158  3anbi2i  1159  3anbi3i  1160  syl3anb  1162  an33rean  1485  cadnot  1615  f13dfv  7294  poxp2  8168  xpord3lem  8174  poxp3  8175  xpord3pred  8177  axgroth5  10864  axgroth6  10868  hash7g  14525  cotr2g  15015  cbvprod  15949  cbvprodv  15950  prodeq1i  15952  isstruct  17189  pmtr3ncomlem1  19491  opprsubg  20352  addscut  28011  mulscut  28158  issubgr  29288  nbgrsym  29380  nb3grpr  29399  cplgr3v  29452  usgr2pthlem  29783  umgr2adedgwlk  29965  umgrwwlks2on  29977  elwspths2spth  29987  clwwlkccat  30009  clwlkclwwlk  30021  3wlkdlem8  30186  frgr3v  30294  or3dir  32479  unelldsys  34159  bnj156  34742  bnj206  34745  bnj887  34779  bnj121  34884  bnj130  34888  bnj605  34921  bnj581  34922  brpprod3b  35888  brapply  35939  brrestrict  35950  dfrdg4  35952  brsegle  36109  prodeq2si  36205  cbvprodvw2  36248  dfeqvrels3  38590  tendoset  40761  grtriproplem  47906  grtrif1o  47909  grlimgrtrilem1  47961  usgrexmpl2trifr  47996  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029
  Copyright terms: Public domain W3C validator