Theorem mpd3an3 1351

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

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

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 983

This theorem is referenced by:  stoic2b  1450  elovmpo  6145  oav  6540  omv  6541  oeiv  6542  f1oeng  6848  mulpipq2  7484  ltrnqg  7533  genipv  7622  subval  8264  subap0  8716  xaddval  9967  fzrevral3  10229  fzoval  10270  subsq2  10792  bcval  10894  ccatws1ls  11094  swrdrlen  11114  dvdsmul1  12124  dvdsmul2  12125  gcdval  12280  eucalgval2  12375  setsvalg  12862  restval  13077  xpsfval  13180  imasmnd2  13284  ismhm  13293  mhmex  13294  subsubm  13315  subsubg  13533  qusinv  13572  isghm  13579  ghminv  13586  rngrz  13708  srglmhm  13755  ringrz  13806  imasring  13826  isrhm  13920  01eq0ring  13951  restin  14648  hmeofvalg  14775  cncfval  15044  rpcxpef  15366  rpcxpneg  15379  sgmval  15455  fsumdvdsmul  15463  lgsval  15481  2lgsoddprmlem4  15589