Theorem mpanr1 709

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  mpanlr1 711  tfr3 3926  oacl 4170  omcl 4171  oaordi 4180  oawordri 4184  oaass 4195  oarec 4196  omordi 4197  omwordri 4203  odi 4210  omass 4211  noinfep 4640  axcnre 5286  divgt0 5857  divge0 5858  recp1lt1 5901  recvalz 6887  climmullem1 7120  climmullem2 7121  climmullem3 7122  climmullem4 7123  cos01gt0 7477  metge0 7819  bopcnlem2 7982  vc2 8174  vc0 8188  vcm 8190  vcnegneg 8193  nvnncan 8283  nvpi 8294  nvge0 8302  sm1cnilem 8347  ipval3 8359  ipid 8363  sspmval 8392  minveclem30 8574  occllem6 9178  nmopcoadj 10034  hstlet 10157  hstrb 10193  atord 10311

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