Theorem ifpor123g

Description: Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020)

	Ref	Expression
Assertion	ifpor123g	|- ( ( 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		df-or	|- ( ( if- ( ph , ch , ta ) \/ if- ( ps , th , et ) ) <-> ( -. if- ( ph , ch , ta ) -> if- ( ps , th , et ) ) )
2		ifpnot23	|- ( -. if- ( ph , ch , ta ) <-> if- ( ph , -. ch , -. ta ) )
3	2	imbi1i	|- ( ( -. if- ( ph , ch , ta ) -> if- ( ps , th , et ) ) <-> ( if- ( ph , -. ch , -. ta ) -> if- ( ps , th , et ) ) )
4	1 3	bitri	|- ( ( if- ( ph , ch , ta ) \/ if- ( ps , th , et ) ) <-> ( if- ( ph , -. ch , -. ta ) -> if- ( ps , th , et ) ) )
5		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 ) ) ) ) )
6	4 5	bitri	|- ( ( if- ( ph , ch , ta ) \/ if- ( ps , th , et ) ) <-> ( ( ( ( ph -> -. ps ) \/ ( -. ch -> th ) ) /\ ( ( ps -> ph ) \/ ( -. ta -> th ) ) ) /\ ( ( ( ph -> ps ) \/ ( -. ch -> et ) ) /\ ( ( -. ps -> ph ) \/ ( -. ta -> et ) ) ) ) )
7		pm4.64	|- ( ( -. ch -> th ) <-> ( ch \/ th ) )
8	7	orbi2i	|- ( ( ( ph -> -. ps ) \/ ( -. ch -> th ) ) <-> ( ( ph -> -. ps ) \/ ( ch \/ th ) ) )
9		pm4.64	|- ( ( -. ta -> th ) <-> ( ta \/ th ) )
10	9	orbi2i	|- ( ( ( ps -> ph ) \/ ( -. ta -> th ) ) <-> ( ( ps -> ph ) \/ ( ta \/ th ) ) )
11	8 10	anbi12i	|- ( ( ( ( ph -> -. ps ) \/ ( -. ch -> th ) ) /\ ( ( ps -> ph ) \/ ( -. ta -> th ) ) ) <-> ( ( ( ph -> -. ps ) \/ ( ch \/ th ) ) /\ ( ( ps -> ph ) \/ ( ta \/ th ) ) ) )
12		pm4.64	|- ( ( -. ch -> et ) <-> ( ch \/ et ) )
13	12	orbi2i	|- ( ( ( ph -> ps ) \/ ( -. ch -> et ) ) <-> ( ( ph -> ps ) \/ ( ch \/ et ) ) )
14		pm4.64	|- ( ( -. ta -> et ) <-> ( ta \/ et ) )
15	14	orbi2i	|- ( ( ( -. ps -> ph ) \/ ( -. ta -> et ) ) <-> ( ( -. ps -> ph ) \/ ( ta \/ et ) ) )
16	13 15	anbi12i	|- ( ( ( ( ph -> ps ) \/ ( -. ch -> et ) ) /\ ( ( -. ps -> ph ) \/ ( -. ta -> et ) ) ) <-> ( ( ( ph -> ps ) \/ ( ch \/ et ) ) /\ ( ( -. ps -> ph ) \/ ( ta \/ et ) ) ) )
17	11 16	anbi12i	|- ( ( ( ( ( ph -> -. ps ) \/ ( -. ch -> th ) ) /\ ( ( ps -> ph ) \/ ( -. ta -> th ) ) ) /\ ( ( ( ph -> ps ) \/ ( -. ch -> et ) ) /\ ( ( -. ps -> ph ) \/ ( -. ta -> et ) ) ) ) <-> ( ( ( ( ph -> -. ps ) \/ ( ch \/ th ) ) /\ ( ( ps -> ph ) \/ ( ta \/ th ) ) ) /\ ( ( ( ph -> ps ) \/ ( ch \/ et ) ) /\ ( ( -. ps -> ph ) \/ ( ta \/ et ) ) ) ) )
18	6 17	bitri	|- ( ( if- ( ph , ch , ta ) \/ if- ( ps , th , et ) ) <-> ( ( ( ( ph -> -. ps ) \/ ( ch \/ th ) ) /\ ( ( ps -> ph ) \/ ( ta \/ th ) ) ) /\ ( ( ( ph -> ps ) \/ ( ch \/ et ) ) /\ ( ( -. ps -> ph ) \/ ( ta \/ et ) ) ) ) )