Theorem mp3an2 1336

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

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

Assertion

Ref	Expression
mp3an2	|- ( ( ph /\ ch ) -> th )

Proof of Theorem mp3an2

Step	Hyp	Ref	Expression
1		mp3an2.1	. 2 |- ps
2		mp3an2.2	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expa 1205	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 435	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  mp3anl2  1343  ordin  4416  ordsuc  4595  omv  6508  oeiv  6509  omv2  6518  1idprl  7650  muladd11  8152  negsub  8267  subneg  8268  ltaddneg  8443  muleqadd  8687  diveqap1  8724  conjmulap  8748  nnsub  9021  addltmul  9219  zltp1le  9371  gtndiv  9412  eluzp1m1  9616  xnn0le2is012  9932  divelunit  10068  fznatpl1  10142  flqbi2  10360  flqdiv  10392  frecfzen2  10498  nn0ennn  10504  seqshft2g  10553  seqf1oglem1  10590  faclbnd3  10814  shftfvalg  10962  ovshftex  10963  shftfval  10965  abs2dif  11250  cos2t  11893  sin01gt0  11905  cos01gt0  11906  demoivre  11916  demoivreALT  11917  omeo  12039  gcd0id  12116  sqgcd  12166  isprm3  12256  eulerthlemth  12370  pczpre  12435  pcrec  12446  setscom  12658  setsslid  12669  setsslnid  12670  mulgm1  13212  abssinper  14981  lgs1  15160