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 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  10817  bcpasc  14360  sqreulem  15398  qnumdencoprm  16782  qeqnumdivden  16783  xpsaddlem  17618  xpsvsca  17622  xpsle  17624  grpinvid  19017  qus0  19207  ghmid  19240  lsm01  19689  frgpadd  19781  abvneg  20827  lsmcv  21143  qusmul2idl  21289  discmp  23406  kgenhaus  23552  idnghm  24764  xmetdcn2  24859  pi1addval  25081  ipcau2  25268  gausslemma2dlem1a  27409  2lgs  27451  etasslt2  27859  uhgrsubgrself  29297  wlkl0  30386  mhmimasplusg  33043  lmhmimasvsca  33044  rlocaddval  33272  rlocmulval  33273  qusvsval  33380  carsgclctunlem2  34321  carsgclctun  34323  ballotlem1ri  34537  satefvfmla0  35423  satefvfmla1  35430  ftc1anclem5  37704  opoc1  39203  opoc0  39204  dochsat  41385  lcfrlem9  41552  fisdomnn  42285  pellfundex  42897  mnringmulrcld  44247  0ellimcdiv  45664  add2cncf  45917  stoweidlem21  46036  stoweidlem23  46038  stoweidlem32  46047  stoweidlem36  46051  stoweidlem40  46055  stoweidlem41  46056  natglobalincr  46892  mod42tp1mod8  47589  lincval0  48332