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  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  7209  1idpr  7407  eqlei2  7865  lem1  8612  eluzfz1  9818  fzpred  9857  uznfz  9890  fz0fzdiffz0  9914  fzctr  9917  flid  10064  flqeqceilz  10098  faclbnd3  10496  bcn1  10511  isfinite4im  10546  leabs  10853  gcd0id  11673  lcmgcdlem  11764  dvdsnprmd  11812  eltpsg  12216  tg1  12237  cldval  12277  cldss  12283  cldopn  12285  psmetdmdm  12502  dvef  12865  relogef  12959  bj-nn0suc0  13201
  Copyright terms: Public domain W3C validator