Theorem mpd3an23 1465

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 1373	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  rankcf  10675  bcpasc  14230  sqreulem  15269  qnumdencoprm  16658  qeqnumdivden  16659  xpsaddlem  17479  xpsvsca  17483  xpsle  17485  grpinvid  18914  qus0  19103  ghmid  19136  lsm01  19585  frgpadd  19677  abvneg  20743  lsmcv  21080  qusmul2idl  21218  discmp  23314  kgenhaus  23460  idnghm  24659  xmetdcn2  24754  pi1addval  24976  ipcau2  25162  gausslemma2dlem1a  27304  2lgs  27346  etasslt2  27756  uhgrsubgrself  29260  wlkl0  30349  mhmimasplusg  33026  lmhmimasvsca  33027  rlocaddval  33242  rlocmulval  33243  qusvsval  33324  carsgclctunlem2  34353  carsgclctun  34355  ballotlem1ri  34569  satefvfmla0  35483  satefvfmla1  35490  ftc1anclem5  37758  opoc1  39322  opoc0  39323  dochsat  41503  lcfrlem9  41670  fisdomnn  42363  pellfundex  43004  mnringmulrcld  44346  0ellimcdiv  45772  add2cncf  46025  stoweidlem21  46144  stoweidlem23  46146  stoweidlem32  46155  stoweidlem36  46159  stoweidlem40  46163  stoweidlem41  46164  natglobalincr  47000  mod42tp1mod8  47727  cycldlenngric  48053  lincval0  48541