Theorem mp3an3 1362

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 1231	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
4	1, 3	mpi 15	1 |- ( ( ph /\ ps ) -> th )

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

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 1006

This theorem is referenced by:  mp3an13  1364  mp3an23  1365  mp3anl3  1369  opelxp  4755  funimaexg  5414  ov  6141  ovmpoa  6152  ovmpo  6157  ovtposg  6425  oaword1  6639  th3q  6809  enrefg  6937  f1imaen  6968  mapxpen  7034  pw1fin  7102  xpfi  7124  djucomen  7431  addnnnq0  7669  mulnnnq0  7670  prarloclemcalc  7722  genpelxp  7731  genpprecll  7734  genppreclu  7735  addsrpr  7965  mulsrpr  7966  gt0srpr  7968  mulrid  8176  ltneg  8642  leneg  8645  suble0  8656  div1  8883  nnaddcl  9163  nnmulcl  9164  nnge1  9166  nnsub  9182  2halves  9373  halfaddsub  9378  addltmul  9381  zleltp1  9535  nnaddm1cl  9541  zextlt  9572  peano5uzti  9588  eluzp1p1  9782  uzaddcl  9820  znq  9858  xrre  10055  xrre2  10056  fzshftral  10343  nninfinf  10705  expn1ap0  10811  expadd  10843  expmul  10846  expubnd  10858  sqmul  10863  bernneq  10922  sqrecapd  10939  faclbnd2  11004  faclbnd6  11006  fihashssdif  11082  ccatlcan  11299  ccatrcan  11300  shftval3  11388  caucvgre  11542  leabs  11635  ltabs  11648  caubnd2  11678  efexp  12244  efival  12294  cos01gt0  12325  odd2np1  12435  halfleoddlt  12456  omoe  12458  opeo  12459  gcdmultiple  12592  sqgcd  12601  nn0seqcvgd  12614  phiprmpw  12795  eulerthlemth  12805  odzcllem  12816  pcelnn  12895  4sqlem3  12964  lsp0  14439  lss0v  14446  zndvds0  14666  ntrin  14850  txuni2  14982  txopn  14991  xblpnfps  15124  xblpnf  15125  bl2in  15129  unirnblps  15148  unirnbl  15149  blpnfctr  15165  plyconst  15471  plyid  15472  sincosq1eq  15565  rpcxpp1  15632  rplogb1  15674