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  2724  ovig  5748  prcdnql  7022  prcunqu  7023  p1le  8282  nnge1  8417  zltp1le  8774  gtndiv  8811  uzss  9008  addlelt  9208  xrre2  9252  xrre3  9253  zltaddlt1le  9392  modfzo0difsn  9767  leexp2r  9974  expnlbnd2  10044  facavg  10119  caubnd2  10515  maxleast  10611  mulcn2  10665  cn1lem  10666  climsqz  10687  climsqz2  10688  climcvg1nlem  10702  fsumabs  10822  zsupcllemstep  11023  gcdzeq  11093  algcvgblem  11113  ialgcvga  11115  lcmdvdsb  11148  coprm  11205
  Copyright terms: Public domain W3C validator