Theorem mpanr1 711

Description: An inference based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mpanr1	|- ((ph /\ ch) -> th)

Proof of Theorem mpanr1

Step	Hyp	Ref	Expression
1		mpanr1.1	. . 3 |- ps
2		mpanr1.2	. . . 4 |- ((ph /\ (ps /\ ch)) -> th)
3	2	ex 373	. . 3 |- (ph -> ((ps /\ ch) -> th))
4	1, 3	mpani 700	. 2 |- (ph -> (ch -> th))
5	4	imp 350	1 |- ((ph /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  mpanlr1 713  tfr3 3933  oacl 4177  omcl 4178  oaordi 4187  oawordri 4191  oaass 4202  oarec 4203  omordi 4204  omwordri 4210  odi 4217  omass 4218  noinfep 4657  axcnre 5305  divgt0 5866  divge0 5867  recp1lt1 5910  recvalz 6894  climmullem1 7127  climmullem2 7128  climmullem3 7129  climmullem4 7130  cos01gt0 7485  metge0 7823  bopcnlem2 7986  vc2 8177  vc0 8191  vcm 8193  vcnegneg 8196  nvnncan 8286  nvpi 8297  nvge0 8305  sm1cnilem 8350  ipval3 8362  ipid 8366  sspmval 8395  minveclem30 8577  occllem6 9180  nmopcoadj 10036  hstlet 10160  hstrb 10196  atord 10314

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