ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpancom Structured version   Unicode 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  6568  eqlei2  6909  lem1  7594  eluzfz1  8665  fzpred  8702  uznfz  8735  fz0fzdiffz0  8757  fzctr  8761  bj-nn0suc0  9410
  Copyright terms: Public domain W3C validator