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

Theorem mpancom 416
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 406 1 (𝜓𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107
This theorem is referenced by:  mpan  418  spesbc  2946  onsucelsucr  4362  sucunielr  4364  ordsuc  4416  peano2b  4466  xpiindim  4614  fvelrnb  5401  fliftcnv  5628  riotaprop  5685  unielxp  6002  dmtpos  6083  tpossym  6103  ercnv  6380  cnvct  6633  php5dom  6686  3xpfi  6748  recrecnq  7103  1idpr  7301  eqlei2  7729  lem1  8463  eluzfz1  9652  fzpred  9691  uznfz  9724  fz0fzdiffz0  9748  fzctr  9751  flid  9898  flqeqceilz  9932  faclbnd3  10330  bcn1  10345  isfinite4im  10380  leabs  10686  gcd0id  11462  lcmgcdlem  11551  dvdsnprmd  11599  eltpsg  11989  tg1  12010  cldval  12050  cldss  12056  cldopn  12058  psmetdmdm  12252  bj-nn0suc0  12733
  Copyright terms: Public domain W3C validator