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  11158  ccatlid  11184  swrd0g  11242  shftfval  11383  mulreap  11426  caucvgrelemrec  11541  binom1p  12048  efi4p  12280  sinadd  12299  cosadd  12300  cos2t  12313  cos2tsin  12314  absefib  12334  efieq1re  12335  demoivreALT  12337  odd2np1  12436  opoe  12458  omoe  12459  opeo  12460  omeo  12461  gcdadd  12558  gcdmultiple  12593  algcvgblem  12623  algcvga  12625  isprm3  12692  coprm  12718  1arith2  12943  rmodislmod  14368  cnfldneg  14590  cnfldmulg  14593  cnfldexp  14594  zringmulg  14615  zringsubgval  14622  bl2ioo  15277  ioo2blex  15279  mpomulcn  15293  sinperlem  15535  logge0  15607  lgsdir2  15765  1lgs  15775