ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpancom Unicode 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  |-  ( ps 
->  ph )
mpancom.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
mpancom  |-  ( ps 
->  ch )

Proof of Theorem mpancom
StepHypRef Expression
1 mpancom.1 . 2  |-  ( ps 
->  ph )
2 id 19 . 2  |-  ( ps 
->  ps )
3 mpancom.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 408 1  |-  ( ps 
->  ch )
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  2966  onsucelsucr  4394  sucunielr  4396  ordsuc  4448  peano2b  4498  xpiindim  4646  fvelrnb  5437  fliftcnv  5664  riotaprop  5721  unielxp  6040  dmtpos  6121  tpossym  6141  ercnv  6418  cnvct  6671  php5dom  6725  3xpfi  6787  recrecnq  7170  1idpr  7368  eqlei2  7826  lem1  8573  eluzfz1  9779  fzpred  9818  uznfz  9851  fz0fzdiffz0  9875  fzctr  9878  flid  10025  flqeqceilz  10059  faclbnd3  10457  bcn1  10472  isfinite4im  10507  leabs  10814  gcd0id  11594  lcmgcdlem  11685  dvdsnprmd  11733  eltpsg  12134  tg1  12155  cldval  12195  cldss  12201  cldopn  12203  psmetdmdm  12420  dvef  12783  bj-nn0suc0  13075
  Copyright terms: Public domain W3C validator