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

Theorem ifpbibib 36124
 Description: Factor conditional logic operator over biimplication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
Assertion
Ref Expression
ifpbibib if- if- if-

Proof of Theorem ifpbibib
StepHypRef Expression
1 dfifp2 1422 . 2 if-
2 dfbi2 632 . . . . . 6
32imbi2i 313 . . . . 5
4 jcab 871 . . . . 5
53, 4bitri 252 . . . 4
6 dfbi2 632 . . . . . 6
76imbi2i 313 . . . . 5
8 jcab 871 . . . . 5
97, 8bitri 252 . . . 4
105, 9anbi12i 701 . . 3
11 an4 831 . . 3
1210, 11bitri 252 . 2
13 dfifp2 1422 . . . . 5 if-
14 ifpimimb 36118 . . . . 5 if- if- if-
1513, 14bitr3i 254 . . . 4 if- if-
16 dfifp2 1422 . . . . 5 if-
17 ifpimimb 36118 . . . . 5 if- if- if-
1816, 17bitr3i 254 . . . 4 if- if-
1915, 18anbi12i 701 . . 3 if- if- if- if-
20 dfbi2 632 . . 3 if- if- if- if- if- if-
2119, 20bitr4i 255 . 2 if- if-
221, 12, 213bitri 274 1 if- if- if-
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370  if-wif 1420 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 188  df-or 371  df-an 372  df-ifp 1421 This theorem is referenced by:  ifpxorxorb  36125
 Copyright terms: Public domain W3C validator