Metamath Proof Explorer
Theorem mpg
Description: Modus ponens combined with generalization. (Contributed by NM, 24May1994)


Ref 
Expression 

Hypotheses 
mpg.1 
$${\u22a2}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi}\to {\psi}$$ 


mpg.2 
$${\u22a2}{\phi}$$ 

Assertion 
mpg 
$${\u22a2}{\psi}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

mpg.1 
$${\u22a2}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi}\to {\psi}$$ 
2 

mpg.2 
$${\u22a2}{\phi}$$ 
3 
2

axgen 
$${\u22a2}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi}$$ 
4 
3 1

axmp 
$${\u22a2}{\psi}$$ 