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

Theorem mpand 429
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 269 . 2  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
41, 3mpan2d 428 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  mpani  430  mp2and  433  rspcimedv  2843  ovig  5995  prcdnql  7482  prcunqu  7483  p1le  8804  nnge1  8940  zltp1le  9305  gtndiv  9346  uzss  9546  addlelt  9766  xrre2  9819  xrre3  9820  zltaddlt1le  10005  modfzo0difsn  10392  leexp2r  10571  expnlbnd2  10642  facavg  10721  caubnd2  11121  maxleast  11217  mulcn2  11315  cn1lem  11317  climsqz  11338  climsqz2  11339  climcvg1nlem  11352  fsumabs  11468  cvgratnnlemnexp  11527  cvgratnnlemmn  11528  zsupcllemstep  11940  gcdzeq  12017  algcvgblem  12043  algcvga  12045  lcmdvdsb  12078  coprm  12138  pclemub  12281  bldisj  13794  xblm  13810  metss2lem  13890  bdxmet  13894  limccoap  14040  lgsne0  14332
  Copyright terms: Public domain W3C validator