NFE Home 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
StepHypRef Expression
1 mpcom.1 . 2 (ψφ)
2 mpcom.2 . . 3 (φ → (ψχ))
32com12 27 . 2 (ψ → (φχ))
41, 3mpd 14 1 (ψχ)
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
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
  Copyright terms: Public domain W3C validator