Theorem mpanr12 778

Description: An inference based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mpanr12	|- (ph -> th)

Proof of Theorem mpanr12

Step	Hyp	Ref	Expression
1		mpanr12.2	. 2 |- ch
2		mpanr12.1	. . 3 |- ps
3		mpanr12.3	. . 3 |- ((ph /\ (ps /\ ch)) -> th)
4	2, 3	mpanr1 774	. 2 |- ((ph /\ ch) -> th)
5	1, 4	mpan2 760	1 |- (ph -> th)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  fprOLD 4811  2dom 5486  limensuci 5600  unfi 5644  cdaen 6073  mulidpq 6221  prlem934a 6289  0idsr 6358  1idsr 6359  00sr 6360  addresr 6408  mulresr 6409  ax0id 6434  ax1id 6435  reclt1 7081  nnleltp1 7138  nominpos 7230  expnass 7886  faclbnd2 8198  climaddlem3 8376  caucvg3lem 8426  erelem3 8583  sin02gt0 8744  blex 9126  opnm 9137  bcthlem1 9277  vacnlem3 9669  minveclem27 9916  minveclem38 9927  sinperlem1 10035  sinq34lt0t 10058  sineq0 10065  efifolem5 10080  efifolem7 10082  mayete3i 11308  mayete3OLDi 11309  lnop0 11527  nmoptrii 11664  nmopcoadji 11671  hstle1 11798  hst0 11805  strlem3a 11824  strlem5 11827  jplem1 11840  wfisg 13917  frinsg 13941  absrdbnd 15799  fdc 15812  totbndbnd 15944

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 164  df-an 242

Copyright terms: Public domain