Theorem mpand 699

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 701  orduniorsuc 3077  xrre2t 5543  p1let 5773  xrmaxltt 5861  maxlet 5866  maxltt 5870  nnge1t 5891  xrsupsslem 6023  xrub 6027  supxrunb1 6036  gtndivt 6140  flwordit 6183  ceilet 6193  qbtwnxr 6217  ser1add2 6275  ser1add 6276  elioc2t 6322  elico2t 6323  elicc2t 6324  uzss 6363  fzss1t 6435  seq1ublem 6848  cvganz 6861  caubnd 6863  caure 6864  cauim 6865  ser1absdiflem 6866  facavgt 6892  bccl2t 6909  fsumsplit 6958  clm3 7017  2climnn 7039  2climnn0 7040  climaddlem3 7052  climmullem8 7063  climsqueeze 7076  climsqueeze2 7077  climabslem 7084  climcau 7092  caucvglem6 7098  caucvg 7099  serzf0 7105  ser1f0 7106  cvgcmp3c 7122  reccnv 7153  cvgratlem4 7188  ivthlem7 7222  ivthlem7OLD 7231  efaddlem23 7302  infpn2 7452  lmnn 7873  iscau3 7876  lmuni 7886  lmcau 7930  bcthlem21 7953  bcthlem25 7957  grpidinvlem3 7984  grpideu 7987  nmcnilem 8272  blocni 8396  minveclem25 8500  minveclem27 8502  htthlem10 8559  hcau2 8976  occllem6 9094  osumlem4 9498  sumspansnt 9511  pjnmop 9986  hmopidmch 9990  atoml 10217  sumdmdlem2 10253  cdj3lem2b 10269

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