Theorem mpd3an23 1464

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  rankcf  10769  bcpasc  14278  sqreulem  15303  qnumdencoprm  16678  qeqnumdivden  16679  xpsaddlem  17516  xpsvsca  17520  xpsle  17522  grpinvid  18881  qus0  19063  ghmid  19093  lsm01  19534  frgpadd  19626  abvneg  20435  lsmcv  20747  qusmul2  20868  discmp  22894  kgenhaus  23040  idnghm  24252  xmetdcn2  24345  pi1addval  24556  ipcau2  24743  gausslemma2dlem1a  26858  2lgs  26900  etasslt2  27305  uhgrsubgrself  28527  wlkl0  29610  qusvsval  32456  qusmul  32504  carsgclctunlem2  33307  carsgclctun  33309  ballotlem1ri  33522  satefvfmla0  34398  satefvfmla1  34405  ftc1anclem5  36554  opoc1  38061  opoc0  38062  dochsat  40243  lcfrlem9  40410  pellfundex  41610  mnringmulrcld  42973  0ellimcdiv  44352  add2cncf  44605  stoweidlem21  44724  stoweidlem23  44726  stoweidlem32  44735  stoweidlem36  44739  stoweidlem40  44743  stoweidlem41  44744  natglobalincr  45578  mod42tp1mod8  46257  lincval0  47050