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

Metamath Proof Explorer

Theorem ex

Description: Exportation inference. (This theorem used to be labeled "exp" but was changed to "ex" so as not to conflict with the math token "exp", per the June 2006 Metamath spec change.) A translation of natural deduction rule -> I ( -> introduction), see natded . (Contributed by NM, 3-Jan-1993) (Proof shortened by Eric Schmidt, 22-Dec-2006)

		Ref	Expression
	Hypothesis	ex.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
	Assertion	ex	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		ex.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
2		df-an	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ¬ ( 𝜑 → ¬ 𝜓 ) )
3	2 1	sylbir	⊢ ( ¬ ( 𝜑 → ¬ 𝜓 ) → 𝜒 )
4	3	expi	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )