Theorem ifpim123g 44485

Description: Implication of conditional logical operators. The right hand side is basically conjunctive normal form which is useful in proofs. (Contributed by RP, 16-Apr-2020.)

Assertion

Ref	Expression
ifpim123g	⊢ ((if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂)))))

Proof of Theorem ifpim123g

Step	Hyp	Ref	Expression
1		dfifp4 1082	. . 3 ⊢ (if-(𝜑, 𝜒, 𝜏) ↔ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)))
2		dfifp4 1082	. . 3 ⊢ (if-(𝜓, 𝜃, 𝜂) ↔ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂)))
3	1, 2	imbi12i 353	. 2 ⊢ ((if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ (((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) → ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂))))
4		imor 867	. 2 ⊢ ((((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) → ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂))) ↔ (¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂))))
5		ordi 1023	. . 3 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂))) ↔ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (¬ 𝜓 ∨ 𝜃)) ∧ (¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (𝜓 ∨ 𝜂))))
6		orass 935	. . . . 5 ⊢ (((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ¬ 𝜓) ∨ 𝜃) ↔ (¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (¬ 𝜓 ∨ 𝜃)))
7		ianor 997	. . . . . . . . . 10 ⊢ (¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ↔ (¬ (¬ 𝜑 ∨ 𝜒) ∨ ¬ (𝜑 ∨ 𝜏)))
8		pm4.52 1000	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝜒) ↔ ¬ (¬ 𝜑 ∨ 𝜒))
9	8	bicomi 227	. . . . . . . . . . 11 ⊢ (¬ (¬ 𝜑 ∨ 𝜒) ↔ (𝜑 ∧ ¬ 𝜒))
10		ioran 999	. . . . . . . . . . 11 ⊢ (¬ (𝜑 ∨ 𝜏) ↔ (¬ 𝜑 ∧ ¬ 𝜏))
11	9, 10	orbi12i 928	. . . . . . . . . 10 ⊢ ((¬ (¬ 𝜑 ∨ 𝜒) ∨ ¬ (𝜑 ∨ 𝜏)) ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (¬ 𝜑 ∧ ¬ 𝜏)))
12		cases2 1063	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝜒) ∨ (¬ 𝜑 ∧ ¬ 𝜏)) ↔ ((𝜑 → ¬ 𝜒) ∧ (¬ 𝜑 → ¬ 𝜏)))
13		imor 867	. . . . . . . . . . . 12 ⊢ ((𝜑 → ¬ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜒))
14		pm4.66 864	. . . . . . . . . . . 12 ⊢ ((¬ 𝜑 → ¬ 𝜏) ↔ (𝜑 ∨ ¬ 𝜏))
15	13, 14	anbi12i 640	. . . . . . . . . . 11 ⊢ (((𝜑 → ¬ 𝜒) ∧ (¬ 𝜑 → ¬ 𝜏)) ↔ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)))
16	12, 15	bitri 278	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝜒) ∨ (¬ 𝜑 ∧ ¬ 𝜏)) ↔ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)))
17	7, 11, 16	3bitri 300	. . . . . . . . 9 ⊢ (¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ↔ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)))
18	17	orbi1i 927	. . . . . . . 8 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ¬ 𝜓) ↔ (((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ ¬ 𝜓))
19		orcom 884	. . . . . . . . 9 ⊢ ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ ¬ 𝜓) ↔ (¬ 𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))))
20		ordi 1023	. . . . . . . . 9 ⊢ ((¬ 𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))) ↔ ((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
21	19, 20	bitri 278	. . . . . . . 8 ⊢ ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ ¬ 𝜓) ↔ ((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
22		orass 935	. . . . . . . . . 10 ⊢ (((¬ 𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ (¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)))
23		orcom 884	. . . . . . . . . . . 12 ⊢ ((¬ 𝜓 ∨ ¬ 𝜑) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
24		imor 867	. . . . . . . . . . . 12 ⊢ ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
25	23, 24	bitr4i 281	. . . . . . . . . . 11 ⊢ ((¬ 𝜓 ∨ ¬ 𝜑) ↔ (𝜑 → ¬ 𝜓))
26	25	orbi1i 927	. . . . . . . . . 10 ⊢ (((¬ 𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ ((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒))
27	22, 26	bitr3i 280	. . . . . . . . 9 ⊢ ((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ↔ ((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒))
28		orass 935	. . . . . . . . . 10 ⊢ (((¬ 𝜓 ∨ 𝜑) ∨ ¬ 𝜏) ↔ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏)))
29		imor 867	. . . . . . . . . . . 12 ⊢ ((𝜓 → 𝜑) ↔ (¬ 𝜓 ∨ 𝜑))
30	29	bicomi 227	. . . . . . . . . . 11 ⊢ ((¬ 𝜓 ∨ 𝜑) ↔ (𝜓 → 𝜑))
31	30	orbi1i 927	. . . . . . . . . 10 ⊢ (((¬ 𝜓 ∨ 𝜑) ∨ ¬ 𝜏) ↔ ((𝜓 → 𝜑) ∨ ¬ 𝜏))
32	28, 31	bitr3i 280	. . . . . . . . 9 ⊢ ((¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏)) ↔ ((𝜓 → 𝜑) ∨ ¬ 𝜏))
33	27, 32	anbi12i 640	. . . . . . . 8 ⊢ (((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏))) ↔ (((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓 → 𝜑) ∨ ¬ 𝜏)))
34	18, 21, 33	3bitri 300	. . . . . . 7 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ¬ 𝜓) ↔ (((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓 → 𝜑) ∨ ¬ 𝜏)))
35	34	orbi1i 927	. . . . . 6 ⊢ (((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ¬ 𝜓) ∨ 𝜃) ↔ ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓 → 𝜑) ∨ ¬ 𝜏)) ∨ 𝜃))
36		ordir 1024	. . . . . 6 ⊢ (((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓 → 𝜑) ∨ ¬ 𝜏)) ∨ 𝜃) ↔ ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ∧ (((𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜃)))
37		orass 935	. . . . . . . 8 ⊢ ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ↔ ((𝜑 → ¬ 𝜓) ∨ (¬ 𝜒 ∨ 𝜃)))
38		imor 867	. . . . . . . . . 10 ⊢ ((𝜒 → 𝜃) ↔ (¬ 𝜒 ∨ 𝜃))
39	38	bicomi 227	. . . . . . . . 9 ⊢ ((¬ 𝜒 ∨ 𝜃) ↔ (𝜒 → 𝜃))
40	39	orbi2i 926	. . . . . . . 8 ⊢ (((𝜑 → ¬ 𝜓) ∨ (¬ 𝜒 ∨ 𝜃)) ↔ ((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)))
41	37, 40	bitri 278	. . . . . . 7 ⊢ ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ↔ ((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)))
42		orass 935	. . . . . . . 8 ⊢ ((((𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜃) ↔ ((𝜓 → 𝜑) ∨ (¬ 𝜏 ∨ 𝜃)))
43		imor 867	. . . . . . . . . 10 ⊢ ((𝜏 → 𝜃) ↔ (¬ 𝜏 ∨ 𝜃))
44	43	bicomi 227	. . . . . . . . 9 ⊢ ((¬ 𝜏 ∨ 𝜃) ↔ (𝜏 → 𝜃))
45	44	orbi2i 926	. . . . . . . 8 ⊢ (((𝜓 → 𝜑) ∨ (¬ 𝜏 ∨ 𝜃)) ↔ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃)))
46	42, 45	bitri 278	. . . . . . 7 ⊢ ((((𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜃) ↔ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃)))
47	41, 46	anbi12i 640	. . . . . 6 ⊢ (((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ∧ (((𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜃)) ↔ (((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))))
48	35, 36, 47	3bitri 300	. . . . 5 ⊢ (((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ¬ 𝜓) ∨ 𝜃) ↔ (((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))))
49	6, 48	bitr3i 280	. . . 4 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (¬ 𝜓 ∨ 𝜃)) ↔ (((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))))
50		orass 935	. . . . 5 ⊢ (((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ 𝜓) ∨ 𝜂) ↔ (¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (𝜓 ∨ 𝜂)))
51	17	orbi1i 927	. . . . . . . 8 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ 𝜓) ↔ (((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ 𝜓))
52		orcom 884	. . . . . . . . 9 ⊢ ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ 𝜓) ↔ (𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))))
53		ordi 1023	. . . . . . . . 9 ⊢ ((𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))) ↔ ((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
54	52, 53	bitri 278	. . . . . . . 8 ⊢ ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ 𝜓) ↔ ((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
55		orass 935	. . . . . . . . . 10 ⊢ (((𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ (𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)))
56		orcom 884	. . . . . . . . . . . 12 ⊢ ((𝜓 ∨ ¬ 𝜑) ↔ (¬ 𝜑 ∨ 𝜓))
57		imor 867	. . . . . . . . . . . 12 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))
58	56, 57	bitr4i 281	. . . . . . . . . . 11 ⊢ ((𝜓 ∨ ¬ 𝜑) ↔ (𝜑 → 𝜓))
59	58	orbi1i 927	. . . . . . . . . 10 ⊢ (((𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ ((𝜑 → 𝜓) ∨ ¬ 𝜒))
60	55, 59	bitr3i 280	. . . . . . . . 9 ⊢ ((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ↔ ((𝜑 → 𝜓) ∨ ¬ 𝜒))
61		orass 935	. . . . . . . . . 10 ⊢ (((𝜓 ∨ 𝜑) ∨ ¬ 𝜏) ↔ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏)))
62		df-or 862	. . . . . . . . . . 11 ⊢ ((𝜓 ∨ 𝜑) ↔ (¬ 𝜓 → 𝜑))
63	62	orbi1i 927	. . . . . . . . . 10 ⊢ (((𝜓 ∨ 𝜑) ∨ ¬ 𝜏) ↔ ((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏))
64	61, 63	bitr3i 280	. . . . . . . . 9 ⊢ ((𝜓 ∨ (𝜑 ∨ ¬ 𝜏)) ↔ ((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏))
65	60, 64	anbi12i 640	. . . . . . . 8 ⊢ (((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏))) ↔ (((𝜑 → 𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏)))
66	51, 54, 65	3bitri 300	. . . . . . 7 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ 𝜓) ↔ (((𝜑 → 𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏)))
67	66	orbi1i 927	. . . . . 6 ⊢ (((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ 𝜓) ∨ 𝜂) ↔ ((((𝜑 → 𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏)) ∨ 𝜂))
68		ordir 1024	. . . . . 6 ⊢ (((((𝜑 → 𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏)) ∨ 𝜂) ↔ ((((𝜑 → 𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ∧ (((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜂)))
69		orass 935	. . . . . . . 8 ⊢ ((((𝜑 → 𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ↔ ((𝜑 → 𝜓) ∨ (¬ 𝜒 ∨ 𝜂)))
70		imor 867	. . . . . . . . . 10 ⊢ ((𝜒 → 𝜂) ↔ (¬ 𝜒 ∨ 𝜂))
71	70	bicomi 227	. . . . . . . . 9 ⊢ ((¬ 𝜒 ∨ 𝜂) ↔ (𝜒 → 𝜂))
72	71	orbi2i 926	. . . . . . . 8 ⊢ (((𝜑 → 𝜓) ∨ (¬ 𝜒 ∨ 𝜂)) ↔ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)))
73	69, 72	bitri 278	. . . . . . 7 ⊢ ((((𝜑 → 𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ↔ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)))
74		orass 935	. . . . . . . 8 ⊢ ((((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜂) ↔ ((¬ 𝜓 → 𝜑) ∨ (¬ 𝜏 ∨ 𝜂)))
75		imor 867	. . . . . . . . . 10 ⊢ ((𝜏 → 𝜂) ↔ (¬ 𝜏 ∨ 𝜂))
76	75	bicomi 227	. . . . . . . . 9 ⊢ ((¬ 𝜏 ∨ 𝜂) ↔ (𝜏 → 𝜂))
77	76	orbi2i 926	. . . . . . . 8 ⊢ (((¬ 𝜓 → 𝜑) ∨ (¬ 𝜏 ∨ 𝜂)) ↔ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂)))
78	74, 77	bitri 278	. . . . . . 7 ⊢ ((((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜂) ↔ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂)))
79	73, 78	anbi12i 640	. . . . . 6 ⊢ (((((𝜑 → 𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ∧ (((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜂)) ↔ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂))))
80	67, 68, 79	3bitri 300	. . . . 5 ⊢ (((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ 𝜓) ∨ 𝜂) ↔ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂))))
81	50, 80	bitr3i 280	. . . 4 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (𝜓 ∨ 𝜂)) ↔ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂))))
82	49, 81	anbi12i 640	. . 3 ⊢ (((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (¬ 𝜓 ∨ 𝜃)) ∧ (¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (𝜓 ∨ 𝜂))) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂)))))
83	5, 82	bitri 278	. 2 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂))) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂)))))
84	3, 4, 83	3bitri 300	1 ⊢ ((if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂)))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861  if-wif 1078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ifp 1079

This theorem is used by:  ifpim1g  44486  ifpbi1b  44488  ifpimimb  44489  ifpor123g  44493  ifpimim  44494