Theorem mpd3an23 1463

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 1371	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  10846  bcpasc  14370  sqreulem  15408  qnumdencoprm  16792  qeqnumdivden  16793  xpsaddlem  17633  xpsvsca  17637  xpsle  17639  grpinvid  19039  qus0  19229  ghmid  19262  lsm01  19713  frgpadd  19805  abvneg  20849  lsmcv  21166  qusmul2idl  21312  discmp  23427  kgenhaus  23573  idnghm  24785  xmetdcn2  24878  pi1addval  25100  ipcau2  25287  gausslemma2dlem1a  27427  2lgs  27469  etasslt2  27877  uhgrsubgrself  29315  wlkl0  30399  mhmimasplusg  33024  lmhmimasvsca  33025  rlocaddval  33240  rlocmulval  33241  qusvsval  33345  carsgclctunlem2  34284  carsgclctun  34286  ballotlem1ri  34499  satefvfmla0  35386  satefvfmla1  35393  ftc1anclem5  37657  opoc1  39158  opoc0  39159  dochsat  41340  lcfrlem9  41507  fisdomnn  42239  pellfundex  42842  mnringmulrcld  44197  0ellimcdiv  45570  add2cncf  45823  stoweidlem21  45942  stoweidlem23  45944  stoweidlem32  45953  stoweidlem36  45957  stoweidlem40  45961  stoweidlem41  45962  natglobalincr  46796  mod42tp1mod8  47476  lincval0  48144