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

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

Proof of Theorem ifpimimb
StepHypRef Expression
1 dfifp2 1427 . 2 if-
2 imor 414 . . . 4
3 pm4.8 367 . . . . . 6
43bicomi 206 . . . . 5
54orbi1i 523 . . . 4
6 id 22 . . . . . 6
76orci 392 . . . . 5
87biantru 508 . . . 4
92, 5, 83bitri 275 . . 3
10 pm4.64 374 . . . 4
11 pm4.81 368 . . . . . 6
1211bicomi 206 . . . . 5
1312orbi1i 523 . . . 4
146orci 392 . . . . 5
1514biantrur 509 . . . 4
1610, 13, 153bitri 275 . . 3
179, 16anbi12i 703 . 2
18 ifpim123g 36144 . . 3 if- if-
1918bicomi 206 . 2 if- if-
201, 17, 193bitri 275 1 if- if- if-
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 188   wo 370   wa 371  if-wif 1425 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 1426 This theorem is referenced by:  ifpororb  36149  ifpbibib  36154
 Copyright terms: Public domain W3C validator