Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpancom 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  2843  onsucelsucr  4234  sucunielr  4236  ordsuc  4287  peano2b  4337  xpiindim  4473  fvelrnb  5221  fliftcnv  5435  riotaprop  5491  unielxp  5800  dmtpos  5871  tpossym  5891  ercnv  6127  php5dom  6325  recrecnq  6492  1idpr  6690  eqlei2  7112  lem1  7813  eluzfz1  8895  fzpred  8932  uznfz  8965  fz0fzdiffz0  8987  fzctr  8991  flid  9126  flqeqceilz  9160  leabs  9672  bj-nn0suc0  10075
 Copyright terms: Public domain W3C validator