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

Metamath Proof Explorer

Theorem bija

Description: Combine antecedents into a single biconditional. This inference, reminiscent of ja , is reversible: The hypotheses can be deduced from the conclusion alone (see pm5.1im and pm5.21im ). (Contributed by Wolf Lammen, 13-May-2013)

	Ref	Expression
Hypotheses	bija.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
	bija.2	⊢ ( ¬ 𝜑 → ( ¬ 𝜓 → 𝜒 ) )
Assertion	bija	⊢ ( ( 𝜑 ↔ 𝜓 ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		bija.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2		bija.2	⊢ ( ¬ 𝜑 → ( ¬ 𝜓 → 𝜒 ) )
3		biimpr	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( 𝜓 → 𝜑 ) )
4	3 1	syli	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( 𝜓 → 𝜒 ) )
5		biimp	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( 𝜑 → 𝜓 ) )
6	5	con3d	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ¬ 𝜓 → ¬ 𝜑 ) )
7	6 2	syli	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ¬ 𝜓 → 𝜒 ) )
8	4 7	pm2.61d	⊢ ( ( 𝜑 ↔ 𝜓 ) → 𝜒 )