Metamath Proof Explorer


Theorem ralbid

Description: Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv . (Contributed by NM, 27-Jun-1998)

Ref Expression
Hypotheses ralbid.1 xφ
ralbid.2 φψχ
Assertion ralbid φxAψxAχ

Proof

Step Hyp Ref Expression
1 ralbid.1 xφ
2 ralbid.2 φψχ
3 2 adantr φxAψχ
4 1 3 ralbida φxAψxAχ