Theorem mpanl1 770

Description: An inference based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mpanl1	|- ((ps /\ ch) -> th)

Proof of Theorem mpanl1

Step	Hyp	Ref	Expression
1		mpanl1.1	. . 3 |- ph
2		mpanl1.2	. . . 4 |- (((ph /\ ps) /\ ch) -> th)
3	2	ex 402	. . 3 |- ((ph /\ ps) -> (ch -> th))
4	1, 3	mpan 759	. 2 |- (ps -> (ch -> th))
5	4	imp 377	1 |- ((ps /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  mpanl12 773  wereu 3654  oeoelem 5273  suppsr3 6376  divdiv23zi 6971  divgt0i 7039  divge0i 7040  ltdiv23i 7077  recp1lt1 7084  crreczi 7991  rimul 7994  recvalzi 8139  clm0ii 8349  climaddlem3 8376  climmullem1 8380  climmullem2 8381  climmullem3 8382  climmullem4 8383  climmullem8 8387  climsub 8390  clim2serzi 8405  climubii 8413  climcaui 8416  cvgcmp2clemOLD 8443  geoisum1c 8507  metge0 9096  methausi 9159  bl2ioo 9189  xplmi 9251  xplm 9253  xpcn 9254  bcthlem7 9283  bcthlem9 9285  bcthlem13 9289  bcthlem19 9295  nmobndi 9777  blometi 9803  blocnilem 9804  ubthlem3 9874  ubthlem9 9880  ubthlem11 9882  minveclem9 9898  minveclem16 9905  minveclem38 9927  spansnm0i 11230  lnopli 11529  lnfnli 11606  nlelchi 11631  opsqrlem1 11711  opsqrlem6 11716  mdslmd3i 11904  atordi 11956  mdsymlem1 11975  elfzp1b 13605  elfzm1b 13606  fnn0ind 13611  mapdiscnlem 14870  frfi 15771  fdc 15812  txmet 15925  heiborlem23 15977  heiborlem32 15986  heiborlem34 15988  pcohtpy 16083  pcorev 16087

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