Theorem mpanl1 716

Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

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

Assertion

Ref	Expression
mpanl1	|- ( ( ps /\ ch ) -> th )

Proof of Theorem mpanl1

Step	Hyp	Ref	Expression
1		mpanl1.1	. . 3 |- ph
2	1	jctl 564	. 2 |- ( ps -> ( ph /\ ps ) )
3		mpanl1.2	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	2, 3	sylan 488	1 |- ( ( ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  mpanl12  718  frc  5080  oeoelem  7678  ercnv  7763  frfi  8205  fin23lem23  9148  divdiv23zi  10778  recp1lt1  10921  divgt0i  10932  divge0i  10933  ltreci  10934  lereci  10935  lt2msqi  10936  le2msqi  10937  msq11i  10938  ltdiv23i  10948  fnn0ind  11476  elfzp1b  12417  elfzm1b  12418  sqrt11i  14124  sqrtmuli  14125  sqrtmsq2i  14127  sqrtlei  14128  sqrtlti  14129  fsum  14451  fprod  14671  blometi  27658  spansnm0i  28509  lnopli  28827  lnfnli  28899  opsqrlem1  28999  opsqrlem6  29004  mdslmd3i  29191  atordi  29243  mdsymlem1  29262  gsummpt2co  29780  finxpreclem4  33231  ptrecube  33409  fdc  33541  prter3  34167