Theorem mpd3an3 1350

Description: An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)

Hypotheses

Ref	Expression
mpd3an3.2	|- ( ( ph /\ ps ) -> ch )
mpd3an3.3	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mpd3an3	|- ( ( ph /\ ps ) -> th )

Proof of Theorem mpd3an3

Step	Hyp	Ref	Expression
1		mpd3an3.2	. 2 |- ( ( ph /\ ps ) -> ch )
2		mpd3an3.3	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expa 1205	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpdan 421	1 |- ( ( ph /\ ps ) -> th )

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

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 982

This theorem is referenced by:  stoic2b  1449  elovmpo  6144  oav  6539  omv  6540  oeiv  6541  f1oeng  6847  mulpipq2  7483  ltrnqg  7532  genipv  7621  subval  8263  subap0  8715  xaddval  9966  fzrevral3  10228  fzoval  10269  subsq2  10790  bcval  10892  dvdsmul1  12066  dvdsmul2  12067  gcdval  12222  eucalgval2  12317  setsvalg  12804  restval  13019  xpsfval  13122  imasmnd2  13226  ismhm  13235  mhmex  13236  subsubm  13257  subsubg  13475  qusinv  13514  isghm  13521  ghminv  13528  rngrz  13650  srglmhm  13697  ringrz  13748  imasring  13768  isrhm  13862  01eq0ring  13893  restin  14590  hmeofvalg  14717  cncfval  14986  rpcxpef  15308  rpcxpneg  15321  sgmval  15397  fsumdvdsmul  15405  lgsval  15423  2lgsoddprmlem4  15531