Theorem mpanl1 705

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 694	. 2 |- (ps -> (ch -> th))
5	4	imp 350	1 |- ((ps /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  mpanl12 707  wereu 2940  suppsr3 5204  recdivt 5754  divgt0 5819  divge0 5820  recp1lt1 5857  ioossre 6336  rimul 6683  recvalz 6833  clm0i 7035  climaddlem3 7060  climmullem1 7064  climmullem2 7065  climmullem3 7066  climmullem4 7067  climmullem8 7071  climsub 7074  clim2serz 7089  climubi 7097  climcau 7100  cvgcmp2clem 7126  geoisum1c 7188  metge0 7771  methausi 7833  bl2ioo 7863  xplmi 7923  xplm 7925  xpcn 7926  bcthlem7 7955  bcthlem9 7957  bcthlem13 7961  bcthlem19 7967  nmobndi 8383  blometi 8407  blocnilem 8408  ubthlem3 8475  ubthlem9 8481  ubthlem11 8483  minveclem9 8497  minveclem16 8504  minveclem38 8526  spansnm0 9535  lnopl 9831  lnfnl 9907  nlelch 9932  mdslmd3 10196  atord 10248  mdsymlem1 10267  mapdiscn 10434

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