Metamath Proof Explorer


Theorem ifcli

Description: Inference associated with ifcl . Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth when the special case B e. C is provable. (Contributed by NM, 14-Aug-1999) (Proof shortened by BJ, 1-Sep-2022)

Ref Expression
Hypotheses ifcli.1 A C
ifcli.2 B C
Assertion ifcli if φ A B C

Proof

Step Hyp Ref Expression
1 ifcli.1 A C
2 ifcli.2 B C
3 ifcl A C B C if φ A B C
4 1 2 3 mp2an if φ A B C