Theorem mpd3an3 1375

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 1230	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpdan 421	1 |- ( ( ph /\ ps ) -> th )

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

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 1007

This theorem is referenced by:  stoic2b  1475  elovmpo  6261  oav  6700  omv  6701  oeiv  6702  f1oeng  7009  mulpipq2  7702  ltrnqg  7751  genipv  7840  subval  8481  subap0  8934  xaddval  10197  fzrevral3  10463  fzoval  10504  subsq2  11033  bcval  11136  ccatws1ls  11355  swrdrlen  11378  pfxpfxid  11426  pfxcctswrd  11427  dvdsmul1  12524  dvdsmul2  12525  gcdval  12680  eucalgval2  12775  setsvalg  13326  restval  13542  xpsfval  13612  imasmnd2  13707  ismhm  13716  mhmex  13717  subsubm  13738  subsubg  13950  qusinv  13989  isghm  13996  ghminv  14003  rngrz  14185  srglmhm  14236  ringrz  14287  imasring  14307  isrhm  14403  01eq0ring  14434  restin  15167  hmeofvalg  15294  cncfval  15563  rpcxpef  15885  rpcxpneg  15898  sgmval  15977  fsumdvdsmul  15985  lgsval  16003  2lgsoddprmlem4  16111  clwwlknon  16550