Theorem mpand 701

Description: A deduction based on modus ponens.

Hypotheses

Ref	Expression
mpand.1	|- (ph -> ps)
mpand.2	|- (ph -> ((ps /\ ch) -> th))

Assertion

Ref	Expression
mpand	|- (ph -> (ch -> th))

Proof of Theorem mpand

Step	Hyp	Ref	Expression
1		mpand.1	. 2 |- (ph -> ps)
2		mpand.2	. . 3 |- (ph -> ((ps /\ ch) -> th))
3	2	exp3a 375	. 2 |- (ph -> (ps -> (ch -> th)))
4	1, 3	mpd 26	1 |- (ph -> (ch -> th))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  mp2and 703  orduniorsuc 3087  xrre2t 5570  p1let 5817  xrmaxltt 5913  maxlet 5918  maxltt 5922  nnge1t 5943  xrsupsslem 6076  xrub 6080  supxrunb1 6089  gtndivt 6193  flwordit 6237  ceilet 6250  qbtwnxr 6279  ser1add2 6338  ser1add 6339  elioc2t 6390  elico2t 6391  elicc2t 6392  uzss 6431  fzss1t 6503  seq1ublem 6911  cvganz 6924  caubnd 6926  caure 6927  cauim 6928  ser1absdiflem 6929  facavgt 6955  bccl2t 6971  fsumsplit 7020  clm3 7079  2climnn 7102  2climnn0 7103  climaddlem3 7116  climmullem8 7127  climsqueeze 7140  climsqueeze2 7141  climabslem 7148  climcau 7156  caucvglem6 7162  caucvg 7163  serzf0 7169  ser1f0 7170  cvgcmp3c 7186  reccnv 7218  cvgratlem4 7253  ivthlem7 7287  efaddlem23 7360  infpn2 7509  lmnn 7935  iscau3 7938  iscau4 7940  lmuni 7951  lmcau 7996  bcthlem21 8019  bcthlem25 8023  grpidinvlem3 8050  grpideu 8053  nmcnilem 8337  blocni 8465  minveclem25 8569  minveclem27 8571  htthlem10 8629  hcau2 9055  occllem6 9178  osumlem4 9581  sumspansnt 9594  pjnmop 10075  hmopidmch 10079  atoml 10309  sumdmdlem2 10346  cdj3lem2b 10364

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain