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  10691  bcpasc  14274  sqreulem  15313  qnumdencoprm  16706  qeqnumdivden  16707  xpsaddlem  17528  xpsvsca  17532  xpsle  17534  grpinvid  18966  qus0  19155  ghmid  19188  lsm01  19637  frgpadd  19729  abvneg  20794  lsmcv  21131  qusmul2idl  21269  discmp  23373  kgenhaus  23519  idnghm  24718  xmetdcn2  24813  pi1addval  25025  ipcau2  25211  gausslemma2dlem1a  27342  2lgs  27384  etaslts2  27800  uhgrsubgrself  29363  wlkl0  30452  mhmimasplusg  33113  lmhmimasvsca  33114  rlocaddval  33344  rlocmulval  33345  qusvsval  33427  carsgclctunlem2  34479  carsgclctun  34481  ballotlem1ri  34695  satefvfmla0  35616  satefvfmla1  35623  ftc1anclem5  38032  opoc1  39662  opoc0  39663  dochsat  41843  lcfrlem9  42010  fisdomnn  42697  pellfundex  43332  mnringmulrcld  44673  0ellimcdiv  46095  add2cncf  46348  stoweidlem21  46467  stoweidlem23  46469  stoweidlem32  46478  stoweidlem36  46482  stoweidlem40  46486  stoweidlem41  46487  natglobalincr  47323  mod42tp1mod8  48077  cycldlenngric  48416  lincval0  48903