Proof of Theorem ifpnannanb
Step | Hyp | Ref
| Expression |
1 | | df-nan 1487 |
. . 3
⊢ ((𝜓 ⊼ 𝜒) ↔ ¬ (𝜓 ∧ 𝜒)) |
2 | | df-nan 1487 |
. . 3
⊢ ((𝜃 ⊼ 𝜏) ↔ ¬ (𝜃 ∧ 𝜏)) |
3 | | ifpbi23 41059 |
. . 3
⊢ ((((𝜓 ⊼ 𝜒) ↔ ¬ (𝜓 ∧ 𝜒)) ∧ ((𝜃 ⊼ 𝜏) ↔ ¬ (𝜃 ∧ 𝜏))) → (if-(𝜑, (𝜓 ⊼ 𝜒), (𝜃 ⊼ 𝜏)) ↔ if-(𝜑, ¬ (𝜓 ∧ 𝜒), ¬ (𝜃 ∧ 𝜏)))) |
4 | 1, 2, 3 | mp2an 689 |
. 2
⊢
(if-(𝜑, (𝜓 ⊼ 𝜒), (𝜃 ⊼ 𝜏)) ↔ if-(𝜑, ¬ (𝜓 ∧ 𝜒), ¬ (𝜃 ∧ 𝜏))) |
5 | | ifpananb 41092 |
. . . 4
⊢
(if-(𝜑, (𝜓 ∧ 𝜒), (𝜃 ∧ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∧ if-(𝜑, 𝜒, 𝜏))) |
6 | 5 | notbii 320 |
. . 3
⊢ (¬
if-(𝜑, (𝜓 ∧ 𝜒), (𝜃 ∧ 𝜏)) ↔ ¬ (if-(𝜑, 𝜓, 𝜃) ∧ if-(𝜑, 𝜒, 𝜏))) |
7 | | ifpnotnotb 41065 |
. . 3
⊢
(if-(𝜑, ¬ (𝜓 ∧ 𝜒), ¬ (𝜃 ∧ 𝜏)) ↔ ¬ if-(𝜑, (𝜓 ∧ 𝜒), (𝜃 ∧ 𝜏))) |
8 | | df-nan 1487 |
. . 3
⊢
((if-(𝜑, 𝜓, 𝜃) ⊼ if-(𝜑, 𝜒, 𝜏)) ↔ ¬ (if-(𝜑, 𝜓, 𝜃) ∧ if-(𝜑, 𝜒, 𝜏))) |
9 | 6, 7, 8 | 3bitr4i 303 |
. 2
⊢
(if-(𝜑, ¬ (𝜓 ∧ 𝜒), ¬ (𝜃 ∧ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊼ if-(𝜑, 𝜒, 𝜏))) |
10 | 4, 9 | bitri 274 |
1
⊢
(if-(𝜑, (𝜓 ⊼ 𝜒), (𝜃 ⊼ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊼ if-(𝜑, 𝜒, 𝜏))) |