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

Theorem mpancom 420
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 409 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  422  spesbc  3040  onsucelsucr  4490  sucunielr  4492  ordsuc  4545  peano2b  4597  xpiindim  4746  fvelrnb  5542  fliftcnv  5772  riotaprop  5830  unielxp  6151  dmtpos  6233  tpossym  6253  ercnv  6531  cnvct  6784  php5dom  6838  3xpfi  6905  recrecnq  7345  1idpr  7543  eqlei2  8003  lem1  8752  eluzfz1  9976  fzpred  10015  uznfz  10048  fz0fzdiffz0  10075  fzctr  10078  flid  10229  flqeqceilz  10263  faclbnd3  10666  bcn1  10681  isfinite4im  10716  leabs  11027  gcd0id  11923  lcmgcdlem  12020  dvdsnprmd  12068  pcprod  12287  fldivp1  12289  intopsn  12610  mgm1  12613  sgrp1  12640  mnd1  12668  mnd1id  12669  eltpsg  12793  tg1  12814  cldval  12854  cldss  12860  cldopn  12862  psmetdmdm  13079  dvef  13443  relogef  13540  zabsle1  13655  bj-nn0suc0  13947
  Copyright terms: Public domain W3C validator