mpcom - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > mpcom		GIF version

Theorem mpcom 32

Description: Modus ponens inference with commutation of antecedents. (Contributed by NM, 17-Mar-1996.)

**Hypotheses**
Ref	Expression
mpcom.1	⊢ (ψ → φ)
mpcom.2	⊢ (φ → (ψ → χ))

**Assertion**
Ref	Expression
mpcom	⊢ (ψ → χ)

**Proof of Theorem mpcom**
Step	Hyp	Ref	Expression
1		mpcom.1	. 2 ⊢ (ψ → φ)
2		mpcom.2	. . 3 ⊢ (φ → (ψ → χ))
3	2	com12 27	. 2 ⊢ (ψ → (φ → χ))
4	1, 3	mpd 14	1 ⊢ (ψ → χ)

Colors of variables: wff setvar class

Syntax hints: → wi 4

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 8

This theorem is referenced by: syldan 456 ax16i 2046 ceqex 2969 unsneqsn 3887 sfintfin 4532 0cnelphi 4597 vtoclr 4816 opeldm 4910 tz6.12-1 5344 tz6.12c 5347 fununiq 5517 oprabid 5550 eloprabga 5578 ndmovordi 5621 clos1conn 5879 enmap2lem3 6065 enmap2 6068 enmap1lem3 6071 enpw 6087 ce0nnuli 6178 fnfrec 6320