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 206  df-an 397  df-3an 1089

This theorem is referenced by:  rankcf  10774  bcpasc  14283  sqreulem  15308  qnumdencoprm  16683  qeqnumdivden  16684  xpsaddlem  17521  xpsvsca  17525  xpsle  17527  grpinvid  18886  qus0  19070  ghmid  19100  lsm01  19541  frgpadd  19633  abvneg  20446  lsmcv  20760  qusmul2  20881  discmp  22909  kgenhaus  23055  idnghm  24267  xmetdcn2  24360  pi1addval  24571  ipcau2  24758  gausslemma2dlem1a  26875  2lgs  26917  etasslt2  27323  uhgrsubgrself  28575  wlkl0  29658  mhmimasplusg  32237  lmhmimasvsca  32238  qusvsval  32508  qusmul  32560  carsgclctunlem2  33387  carsgclctun  33389  ballotlem1ri  33602  satefvfmla0  34478  satefvfmla1  34485  ftc1anclem5  36651  opoc1  38158  opoc0  38159  dochsat  40340  lcfrlem9  40507  pellfundex  41706  mnringmulrcld  43069  0ellimcdiv  44444  add2cncf  44697  stoweidlem21  44816  stoweidlem23  44818  stoweidlem32  44827  stoweidlem36  44831  stoweidlem40  44835  stoweidlem41  44836  natglobalincr  45670  mod42tp1mod8  46349  lincval0  47174