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

Theorem mpancom 407
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 397 1  |-  ( ps 
->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  mpan  408  spesbc  2871  onsucelsucr  4262  sucunielr  4264  ordsuc  4315  peano2b  4365  xpiindim  4501  fvelrnb  5249  fliftcnv  5463  riotaprop  5519  unielxp  5828  dmtpos  5902  tpossym  5922  ercnv  6158  php5dom  6356  recrecnq  6550  1idpr  6748  eqlei2  7171  lem1  7888  eluzfz1  8997  fzpred  9034  uznfz  9067  fz0fzdiffz0  9089  fzctr  9093  flid  9234  flqeqceilz  9268  faclbnd3  9611  bcn1  9626  leabs  9901  bj-nn0suc0  10462
  Copyright terms: Public domain W3C validator