Metamath Proof Explorer

Theorem ifpan123g

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

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

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	anbi12i	\|- ( ( if- ( ph , ch , ta ) /\ if- ( ps , th , et ) ) <-> ( ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) /\ ( ( -. ps \/ th ) /\ ( ps \/ et ) ) ) )

Step

Hyp

Ref

Expression

 |-  ( if- ( ph , ch , ta ) <-> ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) )

 |-  ( if- ( ps , th , et ) <-> ( ( -. ps \/ th ) /\ ( ps \/ et ) ) )

1 2

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