Theorem mp3an2 1366

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mp3anl2  1373  ordin  4530  ordsuc  4710  omv  6728  oeiv  6729  omv2  6738  1idprl  7957  muladd11  8459  negsub  8574  subneg  8575  ltaddneg  8752  muleqadd  8999  diveqap1  9036  conjmulap  9060  nnsub  9344  addltmul  9544  zltp1le  9701  gtndiv  9743  eluzp1m1  9948  xnn0le2is012  10270  divelunit  10406  fznatpl1  10485  flqbi2  10728  flqdiv  10760  frecfzen2  10866  nn0ennn  10872  seqshft2g  10921  seqf1oglem1  10958  faclbnd3  11183  ccatrid  11377  shftfvalg  11585  ovshftex  11586  shftfval  11588  abs2dif  11874  cos2t  12519  sin01gt0  12531  cos01gt0  12532  demoivre  12542  demoivreALT  12543  omeo  12667  gcd0id  12758  sqgcd  12808  isprm3  12898  eulerthlemth  13012  pczpre  13078  pcrec  13089  setscom  13394  setsslid  13405  setsslnid  13406  mulgm1  13947  abssinper  15950  lgs1  16175