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

Theorem 3anbi123i 1243
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 728 . . 3 ((𝜑𝜒) ↔ (𝜓𝜃))
4 bi3.3 . . 3 (𝜏𝜂)
53, 4anbi12i 728 . 2 (((𝜑𝜒) ∧ 𝜏) ↔ ((𝜓𝜃) ∧ 𝜂))
6 df-3an 1032 . 2 ((𝜑𝜒𝜏) ↔ ((𝜑𝜒) ∧ 𝜏))
7 df-3an 1032 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
85, 6, 73bitr4i 290 1 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  3anbi1i  1245  3anbi2i  1246  3anbi3i  1247  syl3anb  1360  an33rean  1437  cadnot  1544  f13dfv  6408  axgroth5  9502  axgroth6  9506  cotr2g  13509  cbvprod  14430  isstruct  15651  pmtr3ncomlem1  17662  opprsubg  18405  nb3grapr  25748  cusgra3v  25759  wwlknfi  26032  frgra3v  26295  or3dir  28498  unelldsys  29354  bnj156  29856  bnj206  29859  bnj887  29895  bnj121  30000  bnj130  30004  bnj605  30037  bnj581  30038  brpprod3b  30970  brapply  31021  brrestrict  31032  dfrdg4  31034  brsegle  31191  tendoset  34868  issubgr  40497  nbgrsym  40593  nb3grpr  40612  usgr2pthlem  40971  umgr2adedgwlk  41154  umgrwwlks2on  41163  elwspths2spth  41173  31wlkdlem8  41336  frgr3v  41447
  Copyright terms: Public domain W3C validator