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

Theorem mpand 423
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 267 . 2  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
41, 3mpan2d 422 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpani  424  mp2and  427  rspcimedv  2763  ovig  5858  prcdnql  7256  prcunqu  7257  p1le  8567  nnge1  8703  zltp1le  9062  gtndiv  9100  uzss  9298  addlelt  9506  xrre2  9555  xrre3  9556  zltaddlt1le  9740  modfzo0difsn  10119  leexp2r  10298  expnlbnd2  10368  facavg  10443  caubnd2  10840  maxleast  10936  mulcn2  11032  cn1lem  11034  climsqz  11055  climsqz2  11056  climcvg1nlem  11069  fsumabs  11185  cvgratnnlemnexp  11244  cvgratnnlemmn  11245  zsupcllemstep  11545  gcdzeq  11617  algcvgblem  11637  algcvga  11639  lcmdvdsb  11672  coprm  11729  bldisj  12476  xblm  12492  metss2lem  12572  bdxmet  12576  limccoap  12722
  Copyright terms: Public domain W3C validator