Theorem mp3an3 1321

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

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

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 975

This theorem is referenced by:  mp3an13  1323  mp3an23  1324  mp3anl3  1328  opelxp  4641  funimaexg  5282  ov  5972  ovmpoa  5983  ovmpo  5988  ovtposg  6238  oaword1  6450  th3q  6618  enrefg  6742  f1imaen  6772  mapxpen  6826  pw1fin  6888  xpfi  6907  djucomen  7193  addnnnq0  7411  mulnnnq0  7412  prarloclemcalc  7464  genpelxp  7473  genpprecll  7476  genppreclu  7477  addsrpr  7707  mulsrpr  7708  gt0srpr  7710  mulid1  7917  ltneg  8381  leneg  8384  suble0  8395  div1  8620  nnaddcl  8898  nnmulcl  8899  nnge1  8901  nnsub  8917  2halves  9107  halfaddsub  9112  addltmul  9114  zleltp1  9267  nnaddm1cl  9273  zextlt  9304  peano5uzti  9320  eluzp1p1  9512  uzaddcl  9545  znq  9583  xrre  9777  xrre2  9778  fzshftral  10064  expn1ap0  10486  expadd  10518  expmul  10521  expubnd  10533  sqmul  10538  bernneq  10596  sqrecapd  10613  faclbnd2  10676  faclbnd6  10678  fihashssdif  10753  shftval3  10791  caucvgre  10945  leabs  11038  ltabs  11051  caubnd2  11081  efexp  11645  efival  11695  cos01gt0  11725  odd2np1  11832  halfleoddlt  11853  omoe  11855  opeo  11856  gcdmultiple  11975  sqgcd  11984  nn0seqcvgd  11995  phiprmpw  12176  eulerthlemth  12186  odzcllem  12196  pcelnn  12274  4sqlem3  12342  ntrin  12918  txuni2  13050  txopn  13059  xblpnfps  13192  xblpnf  13193  bl2in  13197  unirnblps  13216  unirnbl  13217  blpnfctr  13233  sincosq1eq  13554  rpcxpp1  13621  rplogb1  13660