Theorem mp3an1 1335

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 1206	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
4	1, 3	mpan 424	1 |- ( ( ps /\ ch ) -> 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:  mp3an12  1338  mp3an1i  1341  mp3anl1  1342  mp3an  1348  mp3an2i  1353  mp3an3an  1354  tfrlem9  6377  rdgexgg  6436  oaexg  6506  omexg  6509  oeiexg  6511  oav2  6521  nnaordex  6586  mulidnq  7456  1idpru  7658  addgt0sr  7842  muladd11  8159  cnegex  8204  negsubdi  8282  renegcl  8287  mulneg1  8421  ltaddpos  8479  addge01  8499  rimul  8612  recclap  8706  recidap  8713  recidap2  8714  recdivap2  8752  divdiv23apzi  8792  ltmul12a  8887  lemul12a  8889  mulgt1  8890  ltmulgt11  8891  gt0div  8897  ge0div  8898  ltdiv23i  8953  8th4div3  9210  gtndiv  9421  nn0ind  9440  fnn0ind  9442  xrre2  9896  ioorebasg  10050  fzen  10118  elfz0ubfz0  10200  expubnd  10688  le2sq2  10707  bernneq  10752  expnbnd  10755  faclbnd6  10836  bccl  10859  hashfacen  10928  wrdred1hash  10978  shftfval  10986  mulreap  11029  caucvgrelemrec  11144  binom1p  11650  efi4p  11882  sinadd  11901  cosadd  11902  cos2t  11915  cos2tsin  11916  absefib  11936  efieq1re  11937  demoivreALT  11939  odd2np1  12038  opoe  12060  omoe  12061  opeo  12062  omeo  12063  gcdadd  12152  gcdmultiple  12187  algcvgblem  12217  algcvga  12219  isprm3  12286  coprm  12312  1arith2  12537  rmodislmod  13907  cnfldneg  14129  cnfldmulg  14132  cnfldexp  14133  zringmulg  14154  zringsubgval  14161  bl2ioo  14786  ioo2blex  14788  mpomulcn  14802  sinperlem  15044  logge0  15116  lgsdir2  15274  1lgs  15284