Theorem mpd3an3 1379

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  stoic2b  1479  elovmpo  6288  oav  6727  omv  6728  oeiv  6729  f1oeng  7043  mulpipq2  7738  ltrnqg  7787  genipv  7876  subval  8519  subap0  8973  xaddval  10257  fzrevral3  10524  fzoval  10565  subsq2  11097  bcval  11201  ccatws1ls  11424  swrdrlen  11447  pfxpfxid  11495  pfxcctswrd  11496  dvdsmul1  12596  dvdsmul2  12597  gcdval  12752  eucalgval2  12847  setsvalg  13431  restval  13648  xpsfval  13718  imasmnd2  13808  ismhm  13817  mhmex  13818  subsubm  13839  subsubg  14049  qusinv  14088  isghm  14095  ghminv  14102  rngrz  14294  srglmhm  14346  ringrz  14398  imasring  14418  isrhm  14514  01eq0ring  14545  restin  15326  hmeofvalg  15453  cncfval  15722  rpcxpef  16049  rpcxpneg  16062  sgmval  16164  fsumdvdsmul  16186  lgsval  16221  2lgsoddprmlem4  16329  clwwlknon  16768