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  4421  ordsuc  4600  omv  6522  oeiv  6523  omv2  6532  1idprl  7674  muladd11  8176  negsub  8291  subneg  8292  ltaddneg  8468  muleqadd  8712  diveqap1  8749  conjmulap  8773  nnsub  9046  addltmul  9245  zltp1le  9397  gtndiv  9438  eluzp1m1  9642  xnn0le2is012  9958  divelunit  10094  fznatpl1  10168  flqbi2  10398  flqdiv  10430  frecfzen2  10536  nn0ennn  10542  seqshft2g  10591  seqf1oglem1  10628  faclbnd3  10852  shftfvalg  11000  ovshftex  11001  shftfval  11003  abs2dif  11288  cos2t  11932  sin01gt0  11944  cos01gt0  11945  demoivre  11955  demoivreALT  11956  omeo  12080  gcd0id  12171  sqgcd  12221  isprm3  12311  eulerthlemth  12425  pczpre  12491  pcrec  12502  setscom  12743  setsslid  12754  setsslnid  12755  mulgm1  13348  abssinper  15166  lgs1  15369