Mathbox for Richard Penner < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ifpor123g Structured version   Visualization version   Unicode version

Theorem ifpor123g 36164
 Description: Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
Assertion
Ref Expression
ifpor123g if- if-

Proof of Theorem ifpor123g
StepHypRef Expression
1 df-or 372 . . . 4 if- if- if- if-
2 ifpnot23 36134 . . . . 5 if- if-
32imbi1i 327 . . . 4 if- if- if- if-
41, 3bitri 253 . . 3 if- if- if- if-
5 ifpim123g 36156 . . 3 if- if-
64, 5bitri 253 . 2 if- if-
7 pm4.64 374 . . . . 5
87orbi2i 522 . . . 4
9 pm4.64 374 . . . . 5
109orbi2i 522 . . . 4
118, 10anbi12i 704 . . 3
12 pm4.64 374 . . . . 5
1312orbi2i 522 . . . 4
14 pm4.64 374 . . . . 5
1514orbi2i 522 . . . 4
1613, 15anbi12i 704 . . 3
1711, 16anbi12i 704 . 2
186, 17bitri 253 1 if- if-
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 188   wo 370   wa 371  if-wif 1427 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 189  df-or 372  df-an 373  df-ifp 1428 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator