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

Theorem mpand 420
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpand.1  |-  ( ph  ->  ps )
mpand.2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
mpand  |-  ( ph  ->  ( ch  ->  th )
)

Proof of Theorem mpand
StepHypRef Expression
1 mpand.1 . 2  |-  ( ph  ->  ps )
2 mpand.2 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
32ancomsd 265 . 2  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
41, 3mpan2d 419 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mpani  421  mp2and  424  rspcimedv  2712  ovig  5673  prcdnql  6788  prcunqu  6789  p1le  8046  nnge1  8181  zltp1le  8538  gtndiv  8575  uzss  8772  addlelt  8972  xrre2  9016  xrre3  9017  zltaddlt1le  9156  modfzo0difsn  9529  leexp2r  9679  expnlbnd2  9747  facavg  9822  caubnd2  10204  maxleast  10300  mulcn2  10352  cn1lem  10353  climsqz  10374  climsqz2  10375  climcvg1nlem  10387  zsupcllemstep  10548  gcdzeq  10618  algcvgblem  10638  ialgcvga  10640  lcmdvdsb  10673  coprm  10730
  Copyright terms: Public domain W3C validator