Theorem mpd3an3 1374

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

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

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 1006

This theorem is referenced by:  stoic2b  1474  elovmpo  6220  oav  6621  omv  6622  oeiv  6623  f1oeng  6929  mulpipq2  7590  ltrnqg  7639  genipv  7728  subval  8370  subap0  8822  xaddval  10079  fzrevral3  10341  fzoval  10382  subsq2  10908  bcval  11010  ccatws1ls  11218  swrdrlen  11241  pfxpfxid  11289  pfxcctswrd  11290  dvdsmul1  12373  dvdsmul2  12374  gcdval  12529  eucalgval2  12624  setsvalg  13111  restval  13327  xpsfval  13430  imasmnd2  13534  ismhm  13543  mhmex  13544  subsubm  13565  subsubg  13783  qusinv  13822  isghm  13829  ghminv  13836  rngrz  13958  srglmhm  14005  ringrz  14056  imasring  14076  isrhm  14171  01eq0ring  14202  restin  14899  hmeofvalg  15026  cncfval  15295  rpcxpef  15617  rpcxpneg  15630  sgmval  15706  fsumdvdsmul  15714  lgsval  15732  2lgsoddprmlem4  15840  clwwlknon  16279