Theorem mp3an1 1358

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

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

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 1004

This theorem is referenced by:  mp3an12  1361  mp3an1i  1364  mp3anl1  1365  mp3an  1371  mp3an2i  1376  mp3an3an  1377  tfrlem9  6471  rdgexgg  6530  oaexg  6602  omexg  6605  oeiexg  6607  oav2  6617  nnaordex  6682  mulidnq  7587  1idpru  7789  addgt0sr  7973  muladd11  8290  cnegex  8335  negsubdi  8413  renegcl  8418  mulneg1  8552  ltaddpos  8610  addge01  8630  rimul  8743  recclap  8837  recidap  8844  recidap2  8845  recdivap2  8883  divdiv23apzi  8923  ltmul12a  9018  lemul12a  9020  mulgt1  9021  ltmulgt11  9022  gt0div  9028  ge0div  9029  ltdiv23i  9084  8th4div3  9341  gtndiv  9553  nn0ind  9572  fnn0ind  9574  xrre2  10029  ioorebasg  10183  fzen  10251  elfz0ubfz0  10333  expubnd  10830  le2sq2  10849  bernneq  10894  expnbnd  10897  faclbnd6  10978  bccl  11001  hashfacen  11071  wrdred1hash  11128  ccatlid  11154  swrd0g  11208  shftfval  11348  mulreap  11391  caucvgrelemrec  11506  binom1p  12012  efi4p  12244  sinadd  12263  cosadd  12264  cos2t  12277  cos2tsin  12278  absefib  12298  efieq1re  12299  demoivreALT  12301  odd2np1  12400  opoe  12422  omoe  12423  opeo  12424  omeo  12425  gcdadd  12522  gcdmultiple  12557  algcvgblem  12587  algcvga  12589  isprm3  12656  coprm  12682  1arith2  12907  rmodislmod  14331  cnfldneg  14553  cnfldmulg  14556  cnfldexp  14557  zringmulg  14578  zringsubgval  14585  bl2ioo  15240  ioo2blex  15242  mpomulcn  15256  sinperlem  15498  logge0  15570  lgsdir2  15728  1lgs  15738