Metamath Proof Explorer

Theorem ifpidg

Description: Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020)

Ref Expression
Assertion ifpidg ⊢θ↔if-φψχ↔φ∧ψ→θ∧φ∧θ→ψ∧χ→φ∨θ∧θ→φ∨χ

Proof

Step Hyp Ref Expression
1 dfifp4 ⊢if-φψχ↔¬φ∨ψ∧φ∨χ
2 1 bibi2i ⊢θ↔if-φψχ↔θ↔¬φ∨ψ∧φ∨χ
3 dfbi2 ⊢θ↔¬φ∨ψ∧φ∨χ↔θ→¬φ∨ψ∧φ∨χ∧¬φ∨ψ∧φ∨χ→θ
4 imor ⊢θ→¬φ∨ψ∧φ∨χ↔¬θ∨¬φ∨ψ∧φ∨χ
5 ordi ⊢¬θ∨¬φ∨ψ∧φ∨χ↔¬θ∨¬φ∨ψ∧¬θ∨φ∨χ
6 ancomst ⊢φ∧θ→ψ↔θ∧φ→ψ
7 impexp ⊢θ∧φ→ψ↔θ→φ→ψ
8 imor ⊢φ→ψ↔¬φ∨ψ
9 8 imbi2i ⊢θ→φ→ψ↔θ→¬φ∨ψ
10 imor ⊢θ→¬φ∨ψ↔¬θ∨¬φ∨ψ
11 9 10 bitri ⊢θ→φ→ψ↔¬θ∨¬φ∨ψ
12 6 7 11 3bitrri ⊢¬θ∨¬φ∨ψ↔φ∧θ→ψ
13 imor ⊢θ→φ∨χ↔¬θ∨φ∨χ
14 13 bicomi ⊢¬θ∨φ∨χ↔θ→φ∨χ
15 12 14 anbi12i ⊢¬θ∨¬φ∨ψ∧¬θ∨φ∨χ↔φ∧θ→ψ∧θ→φ∨χ
16 4 5 15 3bitri ⊢θ→¬φ∨ψ∧φ∨χ↔φ∧θ→ψ∧θ→φ∨χ
17 8 bicomi ⊢¬φ∨ψ↔φ→ψ
18 df-or ⊢φ∨χ↔¬φ→χ
19 17 18 anbi12i ⊢¬φ∨ψ∧φ∨χ↔φ→ψ∧¬φ→χ
20 cases2 ⊢φ∧ψ∨¬φ∧χ↔φ→ψ∧¬φ→χ
21 20 bicomi ⊢φ→ψ∧¬φ→χ↔φ∧ψ∨¬φ∧χ
22 19 21 bitri ⊢¬φ∨ψ∧φ∨χ↔φ∧ψ∨¬φ∧χ
23 22 imbi1i ⊢¬φ∨ψ∧φ∨χ→θ↔φ∧ψ∨¬φ∧χ→θ
24 jaob ⊢φ∧ψ∨¬φ∧χ→θ↔φ∧ψ→θ∧¬φ∧χ→θ
25 ancomst ⊢¬φ∧χ→θ↔χ∧¬φ→θ
26 pm5.6 ⊢χ∧¬φ→θ↔χ→φ∨θ
27 25 26 bitri ⊢¬φ∧χ→θ↔χ→φ∨θ
28 27 anbi2i ⊢φ∧ψ→θ∧¬φ∧χ→θ↔φ∧ψ→θ∧χ→φ∨θ
29 23 24 28 3bitri ⊢¬φ∨ψ∧φ∨χ→θ↔φ∧ψ→θ∧χ→φ∨θ
30 16 29 anbi12i ⊢θ→¬φ∨ψ∧φ∨χ∧¬φ∨ψ∧φ∨χ→θ↔φ∧θ→ψ∧θ→φ∨χ∧φ∧ψ→θ∧χ→φ∨θ
31 3 30 bitri ⊢θ↔¬φ∨ψ∧φ∨χ↔φ∧θ→ψ∧θ→φ∨χ∧φ∧ψ→θ∧χ→φ∨θ
32 ancom ⊢φ∧θ→ψ∧θ→φ∨χ∧φ∧ψ→θ∧χ→φ∨θ↔φ∧ψ→θ∧χ→φ∨θ∧φ∧θ→ψ∧θ→φ∨χ
33 an4 ⊢φ∧ψ→θ∧χ→φ∨θ∧φ∧θ→ψ∧θ→φ∨χ↔φ∧ψ→θ∧φ∧θ→ψ∧χ→φ∨θ∧θ→φ∨χ
34 32 33 bitri ⊢φ∧θ→ψ∧θ→φ∨χ∧φ∧ψ→θ∧χ→φ∨θ↔φ∧ψ→θ∧φ∧θ→ψ∧χ→φ∨θ∧θ→φ∨χ
35 2 31 34 3bitri ⊢θ↔if-φψχ↔φ∧ψ→θ∧φ∧θ→ψ∧χ→φ∨θ∧θ→φ∨χ