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

Theorem 3anbi123i 1244
 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 729 . . 3 ((𝜑𝜒) ↔ (𝜓𝜃))
4 bi3.3 . . 3 (𝜏𝜂)
53, 4anbi12i 729 . 2 (((𝜑𝜒) ∧ 𝜏) ↔ ((𝜓𝜃) ∧ 𝜂))
6 df-3an 1033 . 2 ((𝜑𝜒𝜏) ↔ ((𝜑𝜒) ∧ 𝜏))
7 df-3an 1033 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
85, 6, 73bitr4i 291 1 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  3anbi1i  1246  3anbi2i  1247  3anbi3i  1248  syl3anb  1361  an33rean  1438  cadnot  1545  f13dfv  6430  axgroth5  9525  axgroth6  9529  cotr2g  13563  cbvprod  14484  isstruct  15705  pmtr3ncomlem1  17716  opprsubg  18459  nb3grapr  25982  cusgra3v  25993  wwlknfi  26266  frgra3v  26529  or3dir  28692  unelldsys  29548  bnj156  30050  bnj206  30053  bnj887  30089  bnj121  30194  bnj130  30198  bnj605  30231  bnj581  30232  brpprod3b  31164  brapply  31215  brrestrict  31226  dfrdg4  31228  brsegle  31385  tendoset  35065  issubgr  40495  nbgrsym  40591  nb3grpr  40610  usgr2pthlem  40969  umgr2adedgwlk  41152  umgrwwlks2on  41161  elwspths2spth  41171  31wlkdlem8  41334  frgr3v  41445
 Copyright terms: Public domain W3C validator