Theorem mp3an3 1337

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an3.1	|- ch
mp3an3.2	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an3	|- ( ( ph /\ ps ) -> th )

Proof of Theorem mp3an3

Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 |- ch
2		mp3an3.2	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expia 1207	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
4	1, 3	mpi 15	1 |- ( ( ph /\ ps ) -> 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:  mp3an13  1339  mp3an23  1340  mp3anl3  1344  opelxp  4694  funimaexg  5343  ov  6046  ovmpoa  6057  ovmpo  6062  ovtposg  6326  oaword1  6538  th3q  6708  enrefg  6832  f1imaen  6862  mapxpen  6918  pw1fin  6980  xpfi  7002  djucomen  7299  addnnnq0  7533  mulnnnq0  7534  prarloclemcalc  7586  genpelxp  7595  genpprecll  7598  genppreclu  7599  addsrpr  7829  mulsrpr  7830  gt0srpr  7832  mulrid  8040  ltneg  8506  leneg  8509  suble0  8520  div1  8747  nnaddcl  9027  nnmulcl  9028  nnge1  9030  nnsub  9046  2halves  9237  halfaddsub  9242  addltmul  9245  zleltp1  9398  nnaddm1cl  9404  zextlt  9435  peano5uzti  9451  eluzp1p1  9644  uzaddcl  9677  znq  9715  xrre  9912  xrre2  9913  fzshftral  10200  nninfinf  10552  expn1ap0  10658  expadd  10690  expmul  10693  expubnd  10705  sqmul  10710  bernneq  10769  sqrecapd  10786  faclbnd2  10851  faclbnd6  10853  fihashssdif  10927  shftval3  11009  caucvgre  11163  leabs  11256  ltabs  11269  caubnd2  11299  efexp  11864  efival  11914  cos01gt0  11945  odd2np1  12055  halfleoddlt  12076  omoe  12078  opeo  12079  gcdmultiple  12212  sqgcd  12221  nn0seqcvgd  12234  phiprmpw  12415  eulerthlemth  12425  odzcllem  12436  pcelnn  12515  4sqlem3  12584  lsp0  14055  lss0v  14062  zndvds0  14282  ntrin  14444  txuni2  14576  txopn  14585  xblpnfps  14718  xblpnf  14719  bl2in  14723  unirnblps  14742  unirnbl  14743  blpnfctr  14759  plyconst  15065  plyid  15066  sincosq1eq  15159  rpcxpp1  15226  rplogb1  15268