Theorem mp3an1 1219

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

Syntax hints:   -> wi 4   /\ wa 97   /\ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  mp3an12  1222  mp3an1i  1225  mp3anl1  1226  mp3an  1232  tfrlem9  5935  rdgexgg  5965  oaexg  6028  omexg  6031  oeiexg  6033  oav2  6043  nnaordex  6100  mulidnq  6487  1idpru  6689  addgt0sr  6860  muladd11  7146  cnegex  7189  negsubdi  7267  renegcl  7272  mulneg1  7392  ltaddpos  7447  addge01  7467  rimul  7576  recclap  7658  recidap  7665  recidap2  7666  recdivap2  7701  divdiv23apzi  7741  ltmul12a  7826  lemul12a  7828  mulgt1  7829  ltmulgt11  7830  gt0div  7836  ge0div  7837  ltdiv23i  7892  8th4div3  8144  gtndiv  8335  nn0ind  8352  fnn0ind  8354  xrre2  8734  ioorebasg  8844  fzen  8907  elfz0ubfz0  8982  frec2uzzd  9186  frec2uzsucd  9187  expubnd  9311  le2sq2  9329  bernneq  9369  expnbnd  9372  shftfval  9422  mulreap  9464  caucvgrelemrec  9578  algcvgblem  9888  ialgcvga  9890