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 1090 . 2 ((𝜑𝜒𝜏) ↔ ((𝜑𝜒) ∧ 𝜏))
7 df-3an 1090 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
85, 6, 73bitr4i 303 1 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  3anbi1i  1158  3anbi2i  1159  3anbi3i  1160  syl3anb  1162  an33rean  1484  an33reanOLD  1485  cadnot  1617  f13dfv  7224  poxp2  8079  xpord3lem  8085  poxp3  8086  xpord3pred  8088  axgroth5  10768  axgroth6  10772  cotr2g  14870  cbvprod  15806  isstruct  17032  pmtr3ncomlem1  19263  opprsubg  20073  issubgr  28268  nbgrsym  28360  nb3grpr  28379  cplgr3v  28432  usgr2pthlem  28760  umgr2adedgwlk  28939  umgrwwlks2on  28951  elwspths2spth  28961  clwwlkccat  28983  clwlkclwwlk  28995  3wlkdlem8  29160  frgr3v  29268  or3dir  31440  unelldsys  32821  bnj156  33404  bnj206  33407  bnj887  33441  bnj121  33546  bnj130  33550  bnj605  33583  bnj581  33584  brpprod3b  34525  brapply  34576  brrestrict  34587  dfrdg4  34589  brsegle  34746  dfeqvrels3  37101  tendoset  39272
  Copyright terms: Public domain W3C validator