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

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

Proof of Theorem ifpananb
StepHypRef Expression
1 anor 497 . . 3
2 anor 497 . . 3
3 ifpbi23 36187 . . 3 if- if-
41, 2, 3mp2an 686 . 2 if- if-
5 ifpororb 36220 . . . . 5 if- if- if-
6 ifpnotnotb 36194 . . . . . 6 if- if-
7 ifpnotnotb 36194 . . . . . 6 if- if-
86, 7orbi12i 530 . . . . 5 if- if- if- if-
95, 8bitri 257 . . . 4 if- if- if-
109notbii 303 . . 3 if- if- if-
11 ifpnotnotb 36194 . . 3 if- if-
12 anor 497 . . 3 if- if- if- if-
1310, 11, 123bitr4i 285 . 2 if- if- if-
144, 13bitri 257 1 if- if- if-
 Colors of variables: wff setvar class Syntax hints:   wn 3   wb 189   wo 375   wa 376  if-wif 983 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 190  df-or 377  df-an 378  df-ifp 984 This theorem is referenced by:  ifpnannanb  36222
 Copyright terms: Public domain W3C validator