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

Theorem mpancom 407
 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 397 1 (𝜓𝜒)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105 This theorem is referenced by:  mpan  408  spesbc  2868  onsucelsucr  4259  sucunielr  4261  ordsuc  4312  peano2b  4362  xpiindim  4498  fvelrnb  5246  fliftcnv  5460  riotaprop  5516  unielxp  5825  dmtpos  5899  tpossym  5919  ercnv  6155  php5dom  6353  recrecnq  6520  1idpr  6718  eqlei2  7141  lem1  7858  eluzfz1  8967  fzpred  9004  uznfz  9037  fz0fzdiffz0  9059  fzctr  9063  flid  9199  flqeqceilz  9233  faclbnd3  9575  bcn1  9590  leabs  9864  bj-nn0suc0  10405
 Copyright terms: Public domain W3C validator