Theorem mp3an2 1303

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 1181	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 431	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  mp3anl2  1310  ordin  4307  ordsuc  4478  omv  6351  oeiv  6352  omv2  6361  1idprl  7398  muladd11  7895  negsub  8010  subneg  8011  ltaddneg  8186  muleqadd  8429  diveqap1  8465  conjmulap  8489  nnsub  8759  addltmul  8956  zltp1le  9108  gtndiv  9146  eluzp1m1  9349  xnn0le2is012  9649  divelunit  9785  fznatpl1  9856  flqbi2  10064  flqdiv  10094  frecfzen2  10200  nn0ennn  10206  faclbnd3  10489  shftfvalg  10590  ovshftex  10591  shftfval  10593  abs2dif  10878  cos2t  11457  sin01gt0  11468  cos01gt0  11469  demoivre  11479  demoivreALT  11480  omeo  11595  gcd0id  11667  sqgcd  11717  isprm3  11799  setscom  11999  setsslid  12009  setsslnid  12010  abssinper  12927