Theorem mpanl1 704

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 373	. . 3 |- ((ph /\ ps) -> (ch -> th))
4	1, 3	mpan 693	. 2 |- (ps -> (ch -> th))
5	4	imp 350	1 |- ((ps /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  mpanl12 706  wereu 2935  suppsr3 5196  recdivt 5746  divgt0 5811  divge0 5812  recp1lt1 5849  ioossre 6328  rimul 6675  recvalz 6825  clm0i 7027  climaddlem3 7052  climmullem1 7056  climmullem2 7057  climmullem3 7058  climmullem4 7059  climmullem8 7063  climsub 7066  clim2serz 7081  climubi 7089  climcau 7092  cvgcmp2clem 7118  geoisum1c 7180  metge0 7760  methausi 7820  bl2ioo 7850  xplmi 7907  xplm 7909  xpcn 7910  bcthlem7 7939  bcthlem9 7941  bcthlem13 7945  bcthlem19 7951  nmobndi 8370  blometi 8394  blocnilem 8395  ubthlem3 8462  ubthlem9 8468  ubthlem11 8470  minveclem9 8484  minveclem16 8491  minveclem38 8513  spansnm0 9512  lnopl 9808  lnfnl 9884  nlelch 9909  mdslmd3 10167  atord 10219  mdsymlem1 10238  mapdiscn 10398

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