Theorem mp3an1 1365

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mp3an12  1368  mp3an1i  1371  mp3anl1  1372  mp3an  1378  mp3an2i  1383  mp3an3an  1384  tfrlem9  6590  rdgexgg  6649  oaexg  6721  omexg  6724  oeiexg  6726  oav2  6736  nnaordex  6801  mulidnq  7756  1idpru  7958  addgt0sr  8142  muladd11  8459  cnegex  8504  negsubdi  8582  renegcl  8587  mulneg1  8722  ltaddpos  8780  addge01  8800  rimul  8913  recclap  9009  recidap  9016  recidap2  9017  recdivap2  9055  divdiv23apzi  9095  ltmul12a  9190  lemul12a  9192  mulgt1  9193  ltmulgt11  9194  gt0div  9200  ge0div  9201  ltdiv23i  9256  8th4div3  9524  gtndiv  9741  nn0ind  9760  fnn0ind  9762  xrre2  10223  ioorebasg  10377  fzen  10447  elfz0ubfz0  10532  expubnd  11033  le2sq2  11052  bernneq  11098  expnbnd  11101  faclbnd6  11182  bccl  11205  hashfibc  11283  hashfacen  11284  wrdred1hash  11348  ccatlid  11374  swrd0g  11432  shftfval  11586  mulreap  11629  caucvgrelemrec  11745  binom1p  12252  efi4p  12484  sinadd  12503  cosadd  12504  cos2t  12517  cos2tsin  12518  absefib  12538  efieq1re  12539  demoivreALT  12541  odd2np1  12640  opoe  12662  omoe  12663  opeo  12664  omeo  12665  gcdadd  12762  gcdmultiple  12797  algcvgblem  12827  algcvga  12829  isprm3  12896  coprm  12922  1arith2  13147  ballotfilem2  13228  rmodislmod  14688  cnfldneg  14910  cnfldmulg  14913  cnfldexp  14914  zringmulg  14933  zringsubgval  14940  bl2ioo  15651  ioo2blex  15653  mpomulcn  15667  sinperlem  15909  logge0  15981  lgsdir2  16152  1lgs  16162