Theorem ifpan23

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

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

Proof

Step	Hyp	Ref	Expression
1		ifpan123g	|- ( ( if- ( ph , ps , ch ) /\ if- ( ph , th , ta ) ) <-> ( ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) /\ ( ( -. ph \/ th ) /\ ( ph \/ ta ) ) ) )
2		an4	|- ( ( ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) /\ ( ( -. ph \/ th ) /\ ( ph \/ ta ) ) ) <-> ( ( ( -. ph \/ ps ) /\ ( -. ph \/ th ) ) /\ ( ( ph \/ ch ) /\ ( ph \/ ta ) ) ) )
3		dfifp4	|- ( if- ( ph , ( ps /\ th ) , ( ch /\ ta ) ) <-> ( ( -. ph \/ ( ps /\ th ) ) /\ ( ph \/ ( ch /\ ta ) ) ) )
4		ordi	|- ( ( -. ph \/ ( ps /\ th ) ) <-> ( ( -. ph \/ ps ) /\ ( -. ph \/ th ) ) )
5		ordi	|- ( ( ph \/ ( ch /\ ta ) ) <-> ( ( ph \/ ch ) /\ ( ph \/ ta ) ) )
6	4 5	anbi12i	|- ( ( ( -. ph \/ ( ps /\ th ) ) /\ ( ph \/ ( ch /\ ta ) ) ) <-> ( ( ( -. ph \/ ps ) /\ ( -. ph \/ th ) ) /\ ( ( ph \/ ch ) /\ ( ph \/ ta ) ) ) )
7	3 6	bitr2i	|- ( ( ( ( -. ph \/ ps ) /\ ( -. ph \/ th ) ) /\ ( ( ph \/ ch ) /\ ( ph \/ ta ) ) ) <-> if- ( ph , ( ps /\ th ) , ( ch /\ ta ) ) )
8	1 2 7	3bitri	|- ( ( if- ( ph , ps , ch ) /\ if- ( ph , th , ta ) ) <-> if- ( ph , ( ps /\ th ) , ( ch /\ ta ) ) )