Theorem mpanr1 707

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  mpanlr1 709  tfr3 3911  oacl 4154  omcl 4155  oaordi 4164  oawordri 4168  oaass 4179  oarec 4180  omordi 4181  omwordri 4187  odi 4194  omass 4195  noinfep 4612  axcnre 5258  divgt0 5811  divge0 5812  recp1lt1 5849  recvalz 6825  climmullem1 7056  climmullem2 7057  climmullem3 7058  climmullem4 7059  cos01gt0 7419  metge0 7760  bopcnlem2 7916  vc2 8111  vc0 8125  vcm 8127  vcnegneg 8130  nvnncan 8223  nvpi 8233  nvge0 8241  sm1cnilem 8281  ipval3 8293  ipid 8297  sspmval 8326  minveclem30 8505  occllem6 9094  nmopcoadj 9948  hstlet 10067  hstrb 10103  atord 10219

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