Theorem mpd3an23 1462

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

This theorem is referenced by:  rankcf  10533  bcpasc  14035  sqreulem  15071  qnumdencoprm  16449  qeqnumdivden  16450  xpsaddlem  17284  xpsvsca  17288  xpsle  17290  grpinvid  18636  qus0  18814  ghmid  18840  lsm01  19277  frgpadd  19369  abvneg  20094  lsmcv  20403  discmp  22549  kgenhaus  22695  idnghm  23907  xmetdcn2  24000  pi1addval  24211  ipcau2  24398  gausslemma2dlem1a  26513  2lgs  26555  uhgrsubgrself  27647  wlkl0  28731  carsgclctunlem2  32286  carsgclctun  32288  ballotlem1ri  32501  satefvfmla0  33380  satefvfmla1  33387  etasslt2  34008  ftc1anclem5  35854  opoc1  37216  opoc0  37217  dochsat  39397  lcfrlem9  39564  pellfundex  40708  mnringmulrcld  41846  0ellimcdiv  43190  add2cncf  43443  stoweidlem21  43562  stoweidlem23  43564  stoweidlem32  43573  stoweidlem36  43577  stoweidlem40  43581  stoweidlem41  43582  mod42tp1mod8  45054  lincval0  45756  natglobalincr  46512