Theorem mpanr1 708

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  mpanlr1 710  tfr3 3917  oacl 4160  omcl 4161  oaordi 4170  oawordri 4174  oaass 4185  oarec 4186  omordi 4187  omwordri 4193  odi 4200  omass 4201  noinfep 4620  axcnre 5266  divgt0 5819  divge0 5820  recp1lt1 5857  recvalz 6833  climmullem1 7064  climmullem2 7065  climmullem3 7066  climmullem4 7067  cos01gt0 7427  metge0 7771  bopcnlem2 7932  vc2 8126  vc0 8140  vcm 8142  vcnegneg 8145  nvnncan 8235  nvpi 8246  nvge0 8254  sm1cnilem 8294  ipval3 8306  ipid 8310  sspmval 8339  minveclem30 8518  occllem6 9117  nmopcoadj 9972  hstlet 10095  hstrb 10131  atord 10248

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