Theorem ifpim123g

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)

	Ref	Expression
Assertion	ifpim123g	|- ( ( if- ( ph , ch , ta ) -> if- ( ps , th , et ) ) <-> ( ( ( ( ph -> -. ps ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( ta -> th ) ) ) /\ ( ( ( ph -> ps ) \/ ( ch -> et ) ) /\ ( ( -. ps -> ph ) \/ ( ta -> et ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfifp4	|- ( if- ( ph , ch , ta ) <-> ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) )
2		dfifp4	|- ( if- ( ps , th , et ) <-> ( ( -. ps \/ th ) /\ ( ps \/ et ) ) )
3	1 2	imbi12i	|- ( ( if- ( ph , ch , ta ) -> if- ( ps , th , et ) ) <-> ( ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) -> ( ( -. ps \/ th ) /\ ( ps \/ et ) ) ) )
4		imor	|- ( ( ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) -> ( ( -. ps \/ th ) /\ ( ps \/ et ) ) ) <-> ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ( ( -. ps \/ th ) /\ ( ps \/ et ) ) ) )
5		ordi	|- ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ( ( -. ps \/ th ) /\ ( ps \/ et ) ) ) <-> ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ( -. ps \/ th ) ) /\ ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ( ps \/ et ) ) ) )
6		orass	|- ( ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ -. ps ) \/ th ) <-> ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ( -. ps \/ th ) ) )
7		ianor	|- ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) <-> ( -. ( -. ph \/ ch ) \/ -. ( ph \/ ta ) ) )
8		pm4.52	|- ( ( ph /\ -. ch ) <-> -. ( -. ph \/ ch ) )
9	8	bicomi	|- ( -. ( -. ph \/ ch ) <-> ( ph /\ -. ch ) )
10		ioran	|- ( -. ( ph \/ ta ) <-> ( -. ph /\ -. ta ) )
11	9 10	orbi12i	|- ( ( -. ( -. ph \/ ch ) \/ -. ( ph \/ ta ) ) <-> ( ( ph /\ -. ch ) \/ ( -. ph /\ -. ta ) ) )
12		cases2	|- ( ( ( ph /\ -. ch ) \/ ( -. ph /\ -. ta ) ) <-> ( ( ph -> -. ch ) /\ ( -. ph -> -. ta ) ) )
13		imor	|- ( ( ph -> -. ch ) <-> ( -. ph \/ -. ch ) )
14		pm4.66	|- ( ( -. ph -> -. ta ) <-> ( ph \/ -. ta ) )
15	13 14	anbi12i	|- ( ( ( ph -> -. ch ) /\ ( -. ph -> -. ta ) ) <-> ( ( -. ph \/ -. ch ) /\ ( ph \/ -. ta ) ) )
16	12 15	bitri	|- ( ( ( ph /\ -. ch ) \/ ( -. ph /\ -. ta ) ) <-> ( ( -. ph \/ -. ch ) /\ ( ph \/ -. ta ) ) )
17	7 11 16	3bitri	|- ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) <-> ( ( -. ph \/ -. ch ) /\ ( ph \/ -. ta ) ) )
18	17	orbi1i	|- ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ -. ps ) <-> ( ( ( -. ph \/ -. ch ) /\ ( ph \/ -. ta ) ) \/ -. ps ) )
19		orcom	|- ( ( ( ( -. ph \/ -. ch ) /\ ( ph \/ -. ta ) ) \/ -. ps ) <-> ( -. ps \/ ( ( -. ph \/ -. ch ) /\ ( ph \/ -. ta ) ) ) )
20		ordi	|- ( ( -. ps \/ ( ( -. ph \/ -. ch ) /\ ( ph \/ -. ta ) ) ) <-> ( ( -. ps \/ ( -. ph \/ -. ch ) ) /\ ( -. ps \/ ( ph \/ -. ta ) ) ) )
21	19 20	bitri	|- ( ( ( ( -. ph \/ -. ch ) /\ ( ph \/ -. ta ) ) \/ -. ps ) <-> ( ( -. ps \/ ( -. ph \/ -. ch ) ) /\ ( -. ps \/ ( ph \/ -. ta ) ) ) )
22		orass	|- ( ( ( -. ps \/ -. ph ) \/ -. ch ) <-> ( -. ps \/ ( -. ph \/ -. ch ) ) )
23		orcom	|- ( ( -. ps \/ -. ph ) <-> ( -. ph \/ -. ps ) )
24		imor	|- ( ( ph -> -. ps ) <-> ( -. ph \/ -. ps ) )
25	23 24	bitr4i	|- ( ( -. ps \/ -. ph ) <-> ( ph -> -. ps ) )
26	25	orbi1i	|- ( ( ( -. ps \/ -. ph ) \/ -. ch ) <-> ( ( ph -> -. ps ) \/ -. ch ) )
27	22 26	bitr3i	|- ( ( -. ps \/ ( -. ph \/ -. ch ) ) <-> ( ( ph -> -. ps ) \/ -. ch ) )
28		orass	|- ( ( ( -. ps \/ ph ) \/ -. ta ) <-> ( -. ps \/ ( ph \/ -. ta ) ) )
29		imor	|- ( ( ps -> ph ) <-> ( -. ps \/ ph ) )
30	29	bicomi	|- ( ( -. ps \/ ph ) <-> ( ps -> ph ) )
31	30	orbi1i	|- ( ( ( -. ps \/ ph ) \/ -. ta ) <-> ( ( ps -> ph ) \/ -. ta ) )
32	28 31	bitr3i	|- ( ( -. ps \/ ( ph \/ -. ta ) ) <-> ( ( ps -> ph ) \/ -. ta ) )
33	27 32	anbi12i	|- ( ( ( -. ps \/ ( -. ph \/ -. ch ) ) /\ ( -. ps \/ ( ph \/ -. ta ) ) ) <-> ( ( ( ph -> -. ps ) \/ -. ch ) /\ ( ( ps -> ph ) \/ -. ta ) ) )
34	18 21 33	3bitri	|- ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ -. ps ) <-> ( ( ( ph -> -. ps ) \/ -. ch ) /\ ( ( ps -> ph ) \/ -. ta ) ) )
35	34	orbi1i	|- ( ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ -. ps ) \/ th ) <-> ( ( ( ( ph -> -. ps ) \/ -. ch ) /\ ( ( ps -> ph ) \/ -. ta ) ) \/ th ) )
36		ordir	|- ( ( ( ( ( ph -> -. ps ) \/ -. ch ) /\ ( ( ps -> ph ) \/ -. ta ) ) \/ th ) <-> ( ( ( ( ph -> -. ps ) \/ -. ch ) \/ th ) /\ ( ( ( ps -> ph ) \/ -. ta ) \/ th ) ) )
37		orass	|- ( ( ( ( ph -> -. ps ) \/ -. ch ) \/ th ) <-> ( ( ph -> -. ps ) \/ ( -. ch \/ th ) ) )
38		imor	|- ( ( ch -> th ) <-> ( -. ch \/ th ) )
39	38	bicomi	|- ( ( -. ch \/ th ) <-> ( ch -> th ) )
40	39	orbi2i	|- ( ( ( ph -> -. ps ) \/ ( -. ch \/ th ) ) <-> ( ( ph -> -. ps ) \/ ( ch -> th ) ) )
41	37 40	bitri	|- ( ( ( ( ph -> -. ps ) \/ -. ch ) \/ th ) <-> ( ( ph -> -. ps ) \/ ( ch -> th ) ) )
42		orass	|- ( ( ( ( ps -> ph ) \/ -. ta ) \/ th ) <-> ( ( ps -> ph ) \/ ( -. ta \/ th ) ) )
43		imor	|- ( ( ta -> th ) <-> ( -. ta \/ th ) )
44	43	bicomi	|- ( ( -. ta \/ th ) <-> ( ta -> th ) )
45	44	orbi2i	|- ( ( ( ps -> ph ) \/ ( -. ta \/ th ) ) <-> ( ( ps -> ph ) \/ ( ta -> th ) ) )
46	42 45	bitri	|- ( ( ( ( ps -> ph ) \/ -. ta ) \/ th ) <-> ( ( ps -> ph ) \/ ( ta -> th ) ) )
47	41 46	anbi12i	|- ( ( ( ( ( ph -> -. ps ) \/ -. ch ) \/ th ) /\ ( ( ( ps -> ph ) \/ -. ta ) \/ th ) ) <-> ( ( ( ph -> -. ps ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( ta -> th ) ) ) )
48	35 36 47	3bitri	|- ( ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ -. ps ) \/ th ) <-> ( ( ( ph -> -. ps ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( ta -> th ) ) ) )
49	6 48	bitr3i	|- ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ( -. ps \/ th ) ) <-> ( ( ( ph -> -. ps ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( ta -> th ) ) ) )
50		orass	|- ( ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ps ) \/ et ) <-> ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ( ps \/ et ) ) )
51	17	orbi1i	|- ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ps ) <-> ( ( ( -. ph \/ -. ch ) /\ ( ph \/ -. ta ) ) \/ ps ) )
52		orcom	|- ( ( ( ( -. ph \/ -. ch ) /\ ( ph \/ -. ta ) ) \/ ps ) <-> ( ps \/ ( ( -. ph \/ -. ch ) /\ ( ph \/ -. ta ) ) ) )
53		ordi	|- ( ( ps \/ ( ( -. ph \/ -. ch ) /\ ( ph \/ -. ta ) ) ) <-> ( ( ps \/ ( -. ph \/ -. ch ) ) /\ ( ps \/ ( ph \/ -. ta ) ) ) )
54	52 53	bitri	|- ( ( ( ( -. ph \/ -. ch ) /\ ( ph \/ -. ta ) ) \/ ps ) <-> ( ( ps \/ ( -. ph \/ -. ch ) ) /\ ( ps \/ ( ph \/ -. ta ) ) ) )
55		orass	|- ( ( ( ps \/ -. ph ) \/ -. ch ) <-> ( ps \/ ( -. ph \/ -. ch ) ) )
56		orcom	|- ( ( ps \/ -. ph ) <-> ( -. ph \/ ps ) )
57		imor	|- ( ( ph -> ps ) <-> ( -. ph \/ ps ) )
58	56 57	bitr4i	|- ( ( ps \/ -. ph ) <-> ( ph -> ps ) )
59	58	orbi1i	|- ( ( ( ps \/ -. ph ) \/ -. ch ) <-> ( ( ph -> ps ) \/ -. ch ) )
60	55 59	bitr3i	|- ( ( ps \/ ( -. ph \/ -. ch ) ) <-> ( ( ph -> ps ) \/ -. ch ) )
61		orass	|- ( ( ( ps \/ ph ) \/ -. ta ) <-> ( ps \/ ( ph \/ -. ta ) ) )
62		df-or	|- ( ( ps \/ ph ) <-> ( -. ps -> ph ) )
63	62	orbi1i	|- ( ( ( ps \/ ph ) \/ -. ta ) <-> ( ( -. ps -> ph ) \/ -. ta ) )
64	61 63	bitr3i	|- ( ( ps \/ ( ph \/ -. ta ) ) <-> ( ( -. ps -> ph ) \/ -. ta ) )
65	60 64	anbi12i	|- ( ( ( ps \/ ( -. ph \/ -. ch ) ) /\ ( ps \/ ( ph \/ -. ta ) ) ) <-> ( ( ( ph -> ps ) \/ -. ch ) /\ ( ( -. ps -> ph ) \/ -. ta ) ) )
66	51 54 65	3bitri	|- ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ps ) <-> ( ( ( ph -> ps ) \/ -. ch ) /\ ( ( -. ps -> ph ) \/ -. ta ) ) )
67	66	orbi1i	|- ( ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ps ) \/ et ) <-> ( ( ( ( ph -> ps ) \/ -. ch ) /\ ( ( -. ps -> ph ) \/ -. ta ) ) \/ et ) )
68		ordir	|- ( ( ( ( ( ph -> ps ) \/ -. ch ) /\ ( ( -. ps -> ph ) \/ -. ta ) ) \/ et ) <-> ( ( ( ( ph -> ps ) \/ -. ch ) \/ et ) /\ ( ( ( -. ps -> ph ) \/ -. ta ) \/ et ) ) )
69		orass	|- ( ( ( ( ph -> ps ) \/ -. ch ) \/ et ) <-> ( ( ph -> ps ) \/ ( -. ch \/ et ) ) )
70		imor	|- ( ( ch -> et ) <-> ( -. ch \/ et ) )
71	70	bicomi	|- ( ( -. ch \/ et ) <-> ( ch -> et ) )
72	71	orbi2i	|- ( ( ( ph -> ps ) \/ ( -. ch \/ et ) ) <-> ( ( ph -> ps ) \/ ( ch -> et ) ) )
73	69 72	bitri	|- ( ( ( ( ph -> ps ) \/ -. ch ) \/ et ) <-> ( ( ph -> ps ) \/ ( ch -> et ) ) )
74		orass	|- ( ( ( ( -. ps -> ph ) \/ -. ta ) \/ et ) <-> ( ( -. ps -> ph ) \/ ( -. ta \/ et ) ) )
75		imor	|- ( ( ta -> et ) <-> ( -. ta \/ et ) )
76	75	bicomi	|- ( ( -. ta \/ et ) <-> ( ta -> et ) )
77	76	orbi2i	|- ( ( ( -. ps -> ph ) \/ ( -. ta \/ et ) ) <-> ( ( -. ps -> ph ) \/ ( ta -> et ) ) )
78	74 77	bitri	|- ( ( ( ( -. ps -> ph ) \/ -. ta ) \/ et ) <-> ( ( -. ps -> ph ) \/ ( ta -> et ) ) )
79	73 78	anbi12i	|- ( ( ( ( ( ph -> ps ) \/ -. ch ) \/ et ) /\ ( ( ( -. ps -> ph ) \/ -. ta ) \/ et ) ) <-> ( ( ( ph -> ps ) \/ ( ch -> et ) ) /\ ( ( -. ps -> ph ) \/ ( ta -> et ) ) ) )
80	67 68 79	3bitri	|- ( ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ps ) \/ et ) <-> ( ( ( ph -> ps ) \/ ( ch -> et ) ) /\ ( ( -. ps -> ph ) \/ ( ta -> et ) ) ) )
81	50 80	bitr3i	|- ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ( ps \/ et ) ) <-> ( ( ( ph -> ps ) \/ ( ch -> et ) ) /\ ( ( -. ps -> ph ) \/ ( ta -> et ) ) ) )
82	49 81	anbi12i	|- ( ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ( -. ps \/ th ) ) /\ ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ( ps \/ et ) ) ) <-> ( ( ( ( ph -> -. ps ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( ta -> th ) ) ) /\ ( ( ( ph -> ps ) \/ ( ch -> et ) ) /\ ( ( -. ps -> ph ) \/ ( ta -> et ) ) ) ) )
83	5 82	bitri	|- ( ( -. ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) \/ ( ( -. ps \/ th ) /\ ( ps \/ et ) ) ) <-> ( ( ( ( ph -> -. ps ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( ta -> th ) ) ) /\ ( ( ( ph -> ps ) \/ ( ch -> et ) ) /\ ( ( -. ps -> ph ) \/ ( ta -> et ) ) ) ) )
84	3 4 83	3bitri	|- ( ( if- ( ph , ch , ta ) -> if- ( ps , th , et ) ) <-> ( ( ( ( ph -> -. ps ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( ta -> th ) ) ) /\ ( ( ( ph -> ps ) \/ ( ch -> et ) ) /\ ( ( -. ps -> ph ) \/ ( ta -> et ) ) ) ) )