Theorem mp3an1 1361

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

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

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 1007

This theorem is referenced by:  mp3an12  1364  mp3an1i  1367  mp3anl1  1368  mp3an  1374  mp3an2i  1379  mp3an3an  1380  tfrlem9  6528  rdgexgg  6587  oaexg  6659  omexg  6662  oeiexg  6664  oav2  6674  nnaordex  6739  mulidnq  7669  1idpru  7871  addgt0sr  8055  muladd11  8371  cnegex  8416  negsubdi  8494  renegcl  8499  mulneg1  8633  ltaddpos  8691  addge01  8711  rimul  8824  recclap  8918  recidap  8925  recidap2  8926  recdivap2  8964  divdiv23apzi  9004  ltmul12a  9099  lemul12a  9101  mulgt1  9102  ltmulgt11  9103  gt0div  9109  ge0div  9110  ltdiv23i  9165  8th4div3  9422  gtndiv  9636  nn0ind  9655  fnn0ind  9657  xrre2  10117  ioorebasg  10271  fzen  10340  elfz0ubfz0  10422  expubnd  10921  le2sq2  10940  bernneq  10985  expnbnd  10988  faclbnd6  11069  bccl  11092  hashfacen  11163  wrdred1hash  11223  ccatlid  11249  swrd0g  11307  shftfval  11461  mulreap  11504  caucvgrelemrec  11619  binom1p  12126  efi4p  12358  sinadd  12377  cosadd  12378  cos2t  12391  cos2tsin  12392  absefib  12412  efieq1re  12413  demoivreALT  12415  odd2np1  12514  opoe  12536  omoe  12537  opeo  12538  omeo  12539  gcdadd  12636  gcdmultiple  12671  algcvgblem  12701  algcvga  12703  isprm3  12770  coprm  12796  1arith2  13021  rmodislmod  14447  cnfldneg  14669  cnfldmulg  14672  cnfldexp  14673  zringmulg  14694  zringsubgval  14701  bl2ioo  15361  ioo2blex  15363  mpomulcn  15377  sinperlem  15619  logge0  15691  lgsdir2  15852  1lgs  15862