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  6484  rdgexgg  6543  oaexg  6615  omexg  6618  oeiexg  6620  oav2  6630  nnaordex  6695  mulidnq  7608  1idpru  7810  addgt0sr  7994  muladd11  8311  cnegex  8356  negsubdi  8434  renegcl  8439  mulneg1  8573  ltaddpos  8631  addge01  8651  rimul  8764  recclap  8858  recidap  8865  recidap2  8866  recdivap2  8904  divdiv23apzi  8944  ltmul12a  9039  lemul12a  9041  mulgt1  9042  ltmulgt11  9043  gt0div  9049  ge0div  9050  ltdiv23i  9105  8th4div3  9362  gtndiv  9574  nn0ind  9593  fnn0ind  9595  xrre2  10055  ioorebasg  10209  fzen  10277  elfz0ubfz0  10359  expubnd  10857  le2sq2  10876  bernneq  10921  expnbnd  10924  faclbnd6  11005  bccl  11028  hashfacen  11099  wrdred1hash  11156  ccatlid  11182  swrd0g  11240  shftfval  11381  mulreap  11424  caucvgrelemrec  11539  binom1p  12045  efi4p  12277  sinadd  12296  cosadd  12297  cos2t  12310  cos2tsin  12311  absefib  12331  efieq1re  12332  demoivreALT  12334  odd2np1  12433  opoe  12455  omoe  12456  opeo  12457  omeo  12458  gcdadd  12555  gcdmultiple  12590  algcvgblem  12620  algcvga  12622  isprm3  12689  coprm  12715  1arith2  12940  rmodislmod  14364  cnfldneg  14586  cnfldmulg  14589  cnfldexp  14590  zringmulg  14611  zringsubgval  14618  bl2ioo  15273  ioo2blex  15275  mpomulcn  15289  sinperlem  15531  logge0  15603  lgsdir2  15761  1lgs  15771