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

Theorem mpancom 414
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 404 1  |-  ( ps 
->  ch )
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  416  spesbc  2927  onsucelsucr  4340  sucunielr  4342  ordsuc  4394  peano2b  4444  xpiindim  4588  fvelrnb  5367  fliftcnv  5590  riotaprop  5647  unielxp  5960  dmtpos  6037  tpossym  6057  ercnv  6329  cnvct  6582  php5dom  6635  3xpfi  6697  recrecnq  7016  1idpr  7214  eqlei2  7642  lem1  8371  eluzfz1  9508  fzpred  9547  uznfz  9580  fz0fzdiffz0  9604  fzctr  9607  flid  9754  flqeqceilz  9788  faclbnd3  10214  bcn1  10229  isfinite4im  10264  leabs  10570  gcd0id  11311  lcmgcdlem  11400  dvdsnprmd  11448  eltpsg  11801  tg1  11822  cldval  11862  cldss  11868  cldopn  11870  bj-nn0suc0  12149
  Copyright terms: Public domain W3C validator