Theorem ex-natded5.2i

Description: The same as ex-natded5.2 and ex-natded5.2-2 but with no context. (Contributed by Mario Carneiro, 9-Feb-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ex-natded5.2i.1	$$⊢\left(\psi \wedge \chi \right)\to \theta$$
	ex-natded5.2i.2	$$⊢\chi \to \psi$$
	ex-natded5.2i.3	$$⊢\chi$$
Assertion	ex-natded5.2i	$$⊢\theta$$

Proof

Step	Hyp	Ref	Expression
1		ex-natded5.2i.1	$$⊢\left(\psi \wedge \chi \right)\to \theta$$
2		ex-natded5.2i.2	$$⊢\chi \to \psi$$
3		ex-natded5.2i.3	$$⊢\chi$$
4	3 2	ax-mp	$$⊢\psi$$
5	4 3	pm3.2i	$$⊢\left(\psi \wedge \chi \right)$$
6	5 1	ax-mp	$$⊢\theta$$