Theorem mp3an2 1359

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

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

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 1004

This theorem is referenced by:  mp3anl2  1366  ordin  4476  ordsuc  4655  omv  6609  oeiv  6610  omv2  6619  1idprl  7785  muladd11  8287  negsub  8402  subneg  8403  ltaddneg  8579  muleqadd  8823  diveqap1  8860  conjmulap  8884  nnsub  9157  addltmul  9356  zltp1le  9509  gtndiv  9550  eluzp1m1  9754  xnn0le2is012  10070  divelunit  10206  fznatpl1  10280  flqbi2  10519  flqdiv  10551  frecfzen2  10657  nn0ennn  10663  seqshft2g  10712  seqf1oglem1  10749  faclbnd3  10973  ccatrid  11150  shftfvalg  11337  ovshftex  11338  shftfval  11340  abs2dif  11625  cos2t  12269  sin01gt0  12281  cos01gt0  12282  demoivre  12292  demoivreALT  12293  omeo  12417  gcd0id  12508  sqgcd  12558  isprm3  12648  eulerthlemth  12762  pczpre  12828  pcrec  12839  setscom  13080  setsslid  13091  setsslnid  13092  mulgm1  13687  abssinper  15528  lgs1  15731