Theorem mp3an1 1360

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

Hypotheses

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

Assertion

Ref	Expression
mp3an1	|- ( ( ps /\ ch ) -> th )

Proof of Theorem mp3an1

Step	Hyp	Ref	Expression
1		mp3an1.1	. 2 |- ph
2		mp3an1.2	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expb 1230	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
4	1, 3	mpan 424	1 |- ( ( ps /\ ch ) -> 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:  mp3an12  1363  mp3an1i  1366  mp3anl1  1367  mp3an  1373  mp3an2i  1378  mp3an3an  1379  tfrlem9  6485  rdgexgg  6544  oaexg  6616  omexg  6619  oeiexg  6621  oav2  6631  nnaordex  6696  mulidnq  7609  1idpru  7811  addgt0sr  7995  muladd11  8312  cnegex  8357  negsubdi  8435  renegcl  8440  mulneg1  8574  ltaddpos  8632  addge01  8652  rimul  8765  recclap  8859  recidap  8866  recidap2  8867  recdivap2  8905  divdiv23apzi  8945  ltmul12a  9040  lemul12a  9042  mulgt1  9043  ltmulgt11  9044  gt0div  9050  ge0div  9051  ltdiv23i  9106  8th4div3  9363  gtndiv  9575  nn0ind  9594  fnn0ind  9596  xrre2  10056  ioorebasg  10210  fzen  10278  elfz0ubfz0  10360  expubnd  10859  le2sq2  10878  bernneq  10923  expnbnd  10926  faclbnd6  11007  bccl  11030  hashfacen  11101  wrdred1hash  11161  ccatlid  11187  swrd0g  11245  shftfval  11399  mulreap  11442  caucvgrelemrec  11557  binom1p  12064  efi4p  12296  sinadd  12315  cosadd  12316  cos2t  12329  cos2tsin  12330  absefib  12350  efieq1re  12351  demoivreALT  12353  odd2np1  12452  opoe  12474  omoe  12475  opeo  12476  omeo  12477  gcdadd  12574  gcdmultiple  12609  algcvgblem  12639  algcvga  12641  isprm3  12708  coprm  12734  1arith2  12959  rmodislmod  14384  cnfldneg  14606  cnfldmulg  14609  cnfldexp  14610  zringmulg  14631  zringsubgval  14638  bl2ioo  15293  ioo2blex  15295  mpomulcn  15309  sinperlem  15551  logge0  15623  lgsdir2  15781  1lgs  15791