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  ccatws1ls  11092  dvdsmul1  12095  dvdsmul2  12096  gcdval  12251  eucalgval2  12346  setsvalg  12833  restval  13048  xpsfval  13151  imasmnd2  13255  ismhm  13264  mhmex  13265  subsubm  13286  subsubg  13504  qusinv  13543  isghm  13550  ghminv  13557  rngrz  13679  srglmhm  13726  ringrz  13777  imasring  13797  isrhm  13891  01eq0ring  13922  restin  14619  hmeofvalg  14746  cncfval  15015  rpcxpef  15337  rpcxpneg  15350  sgmval  15426  fsumdvdsmul  15434  lgsval  15452  2lgsoddprmlem4  15560