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  8460  cnegex  8505  negsubdi  8583  renegcl  8588  mulneg1  8723  ltaddpos  8781  addge01  8801  rimul  8915  recclap  9011  recidap  9018  recidap2  9019  recdivap2  9057  divdiv23apzi  9097  ltmul12a  9192  lemul12a  9194  mulgt1  9195  ltmulgt11  9196  gt0div  9202  ge0div  9203  ltdiv23i  9258  8th4div3  9528  gtndiv  9745  nn0ind  9764  fnn0ind  9766  xrre2  10233  ioorebasg  10387  fzen  10457  elfz0ubfz0  10542  expubnd  11046  le2sq2  11065  bernneq  11111  expnbnd  11114  faclbnd6  11196  bccl  11219  hashfibc  11297  hashfacen  11298  wrdred1hash  11362  ccatlid  11388  swrd0g  11446  shftfval  11600  mulreap  11643  caucvgrelemrec  11759  binom1p  12268  efi4p  12500  sinadd  12519  cosadd  12520  cos2t  12533  cos2tsin  12534  absefib  12554  efieq1re  12555  demoivreALT  12557  odd2np1  12656  opoe  12678  omoe  12679  opeo  12680  omeo  12681  gcdadd  12778  gcdmultiple  12813  algcvgblem  12843  algcvga  12845  isprm3  12912  coprm  12939  1arith2  13167  ballotfilem2  13277  rmodislmod  14737  cnfldneg  14959  cnfldmulg  14962  cnfldexp  14963  zringmulg  14982  zringsubgval  14989  bl2ioo  15700  ioo2blex  15702  mpomulcn  15716  sinperlem  15959  logge0  16032  ppiqnncl  16181  bposlem2  16210  lgsdir2  16250  1lgs  16260