Theorem mp3an2 1304

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

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

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 965

This theorem is referenced by:  mp3anl2  1311  ordin  4315  ordsuc  4486  omv  6359  oeiv  6360  omv2  6369  1idprl  7422  muladd11  7919  negsub  8034  subneg  8035  ltaddneg  8210  muleqadd  8453  diveqap1  8489  conjmulap  8513  nnsub  8783  addltmul  8980  zltp1le  9132  gtndiv  9170  eluzp1m1  9373  xnn0le2is012  9679  divelunit  9815  fznatpl1  9887  flqbi2  10095  flqdiv  10125  frecfzen2  10231  nn0ennn  10237  faclbnd3  10521  shftfvalg  10622  ovshftex  10623  shftfval  10625  abs2dif  10910  cos2t  11493  sin01gt0  11504  cos01gt0  11505  demoivre  11515  demoivreALT  11516  omeo  11631  gcd0id  11703  sqgcd  11753  isprm3  11835  setscom  12038  setsslid  12048  setsslnid  12049  abssinper  12975