ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpancom Structured version   GIF version

Theorem mpancom 399
Description: An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpancom.1 (ψφ)
mpancom.2 ((φ ψ) → χ)
Assertion
Ref Expression
mpancom (ψχ)

Proof of Theorem mpancom
StepHypRef Expression
1 mpancom.1 . 2 (ψφ)
2 id 19 . 2 (ψψ)
3 mpancom.2 . 2 ((φ ψ) → χ)
41, 2, 3syl2anc 391 1 (ψχ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  mpan  400  spesbc  2837  onsucelsucr  4199  sucunielr  4201  ordsuc  4241  peano2b  4280  xpiindim  4416  fvelrnb  5164  fliftcnv  5378  riotaprop  5434  unielxp  5742  dmtpos  5812  tpossym  5832  ercnv  6063  recrecnq  6378  1idpr  6566  eqlei2  6869  lem1  7554  eluzfz1  8625  fzpred  8662  uznfz  8695  fz0fzdiffz0  8717  fzctr  8721  bj-nn0suc0  9338
  Copyright terms: Public domain W3C validator