Metamath Proof Explorer


Theorem ifcl

Description: Membership (closure) of a conditional operator. (Contributed by NM, 4-Apr-2005)

Ref Expression
Assertion ifcl A C B C if φ A B C

Proof

Step Hyp Ref Expression
1 eleq1 A = if φ A B A C if φ A B C
2 eleq1 B = if φ A B B C if φ A B C
3 1 2 ifboth A C B C if φ A B C