Theorem mpand 765

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 405	. 2 |- (ph -> (ps -> (ch -> th)))
4	1, 3	mpd 29	1 |- (ph -> (ch -> th))

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  mp2and 767  orduniorsuc 3909  xrre2 6745  p1le 6995  xrmaxlt 7096  maxle 7101  maxlt 7105  nnge1 7126  xrsupsslem 7285  xrub 7289  supxrunb1 7298  gtndiv 7405  qbtwnxr 7460  flwordi 7477  ceile 7491  elioc2 7558  elico2 7559  elicc2 7560  uzss 7600  fzss1 7675  ser1add2i 7751  ser1addi 7752  expnlbnd2 7903  seq1ublem 8163  cvganz 8176  caubndi 8178  caurei 8179  cauimi 8180  ser1absdiflem 8181  facavg 8207  bccl2 8223  fsumsplit 8280  clm3i 8339  2climnn 8362  2climnn0 8363  climaddlem3 8376  climmullem8 8387  climsqueeze 8400  climsqueeze2 8401  climabslem 8408  climcaui 8416  caucvglem6 8422  caucvgi 8423  serzf0i 8429  cvgcmp3ci 8447  reccnv 8479  cvgratlem4 8515  ivthlem7 8549  efaddlem23 8622  infpn2 8778  lmnn 9213  iscau3 9216  iscau4 9218  lmuni 9229  lmcau 9274  bcthlem21 9297  bcthlem25 9301  grpidinvlem3 9330  grpideu 9333  nmcnilem 9676  blocni 9805  minveclem25 9914  minveclem27 9916  htthlem10 9976  findcardOLD 10179  hcau2 10688  occllem6 10811  osumlem4 11216  sumspansn 11229  pjnmopi 11719  hmopidmchi 11723  atomli 11954  sumdmdlem2 11991  cdj3lem2b 12009  algcvgblem 13745  algcvga 13747  coprm 13782  coprmdvds 13783  dfon2lem5 13853  dfon2lem6 13854  eluzadd 15782  uzm1 15784  metdcn 15853  icoopnst 15876  iocopnst 15877  lmtlm 15908  totbndbnd 15944  heiborlem32 15986  heiborlem35 15989  heiborlem36 15990  bfplem6 16003  rrncms 16019  divrngidl 16176  strssp1 16713  fnelstr 16717  lubid 16807  joinle 16820  meetle 16827  latmlem1 16876  lecmt 16977  grpidinvlem3NEW 17111  grpideuNEW 17114  osumcllem11 17374  pexmidlem8 17385

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 164  df-an 242

Copyright terms: Public domain