This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
ex-natded5.2i.2 ⊢ ( 𝜒 → 𝜓 )
ex-natded5.2i.3 ⊢ 𝜒
Assertion ex-natded5.2i 𝜃

Proof

Step Hyp Ref Expression
1 ex-natded5.2i.1 ⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
2 ex-natded5.2i.2 ⊢ ( 𝜒 → 𝜓 )
3 ex-natded5.2i.3 ⊢ 𝜒
4 3 2 ax-mp ⊢ 𝜓
5 4 3 pm3.2i ⊢ ( 𝜓 ∧ 𝜒 )
6 5 1 ax-mp ⊢ 𝜃