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

Theorem mpancom 418
 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 408 1 (𝜓𝜒)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107 This theorem is referenced by:  mpan  420  spesbc  2994  onsucelsucr  4424  sucunielr  4426  ordsuc  4478  peano2b  4528  xpiindim  4676  fvelrnb  5469  fliftcnv  5696  riotaprop  5753  unielxp  6072  dmtpos  6153  tpossym  6173  ercnv  6450  cnvct  6703  php5dom  6757  3xpfi  6819  recrecnq  7216  1idpr  7414  eqlei2  7872  lem1  8619  eluzfz1  9825  fzpred  9864  uznfz  9897  fz0fzdiffz0  9921  fzctr  9924  flid  10071  flqeqceilz  10105  faclbnd3  10503  bcn1  10518  isfinite4im  10553  leabs  10860  gcd0id  11680  lcmgcdlem  11771  dvdsnprmd  11819  eltpsg  12223  tg1  12244  cldval  12284  cldss  12290  cldopn  12292  psmetdmdm  12509  dvef  12873  relogef  12969  bj-nn0suc0  13255
 Copyright terms: Public domain W3C validator