Metamath Proof Explorer


Theorem jao1i

Description: Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010)

Ref Expression
Hypothesis jao1i.1 ψχφ
Assertion jao1i φψχφ

Proof

Step Hyp Ref Expression
1 jao1i.1 ψχφ
2 ax-1 φχφ
3 2 1 jaoi φψχφ