Theorem mpd3an23 1466

Description: An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.)

Hypotheses

Ref	Expression
mpd3an23.1	⊢ (𝜑 → 𝜓)
mpd3an23.2	⊢ (𝜑 → 𝜒)
mpd3an23.3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mpd3an23	⊢ (𝜑 → 𝜃)

Proof of Theorem mpd3an23

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2		mpd3an23.1	. 2 ⊢ (𝜑 → 𝜓)
3		mpd3an23.2	. 2 ⊢ (𝜑 → 𝜒)
4		mpd3an23.3	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
5	1, 2, 3, 4	syl3anc 1374	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089

This theorem is referenced by:  rankcf  10700  bcpasc  14256  sqreulem  15295  qnumdencoprm  16684  qeqnumdivden  16685  xpsaddlem  17506  xpsvsca  17510  xpsle  17512  grpinvid  18941  qus0  19130  ghmid  19163  lsm01  19612  frgpadd  19704  abvneg  20771  lsmcv  21108  qusmul2idl  21246  discmp  23354  kgenhaus  23500  idnghm  24699  xmetdcn2  24794  pi1addval  25016  ipcau2  25202  gausslemma2dlem1a  27344  2lgs  27386  etaslts2  27802  uhgrsubgrself  29365  wlkl0  30454  mhmimasplusg  33130  lmhmimasvsca  33131  rlocaddval  33361  rlocmulval  33362  qusvsval  33444  carsgclctunlem2  34496  carsgclctun  34498  ballotlem1ri  34712  satefvfmla0  35631  satefvfmla1  35638  ftc1anclem5  37942  opoc1  39572  opoc0  39573  dochsat  41753  lcfrlem9  41920  fisdomnn  42608  pellfundex  43237  mnringmulrcld  44578  0ellimcdiv  46001  add2cncf  46254  stoweidlem21  46373  stoweidlem23  46375  stoweidlem32  46384  stoweidlem36  46388  stoweidlem40  46392  stoweidlem41  46393  natglobalincr  47229  mod42tp1mod8  47956  cycldlenngric  48282  lincval0  48769