Theorem mpd3an23 1460

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  rankcf  10801  bcpasc  14313  sqreulem  15339  qnumdencoprm  16717  qeqnumdivden  16718  xpsaddlem  17555  xpsvsca  17559  xpsle  17561  grpinvid  18956  qus0  19144  ghmid  19176  lsm01  19626  frgpadd  19718  abvneg  20714  lsmcv  21029  qusmul2  21171  discmp  23315  kgenhaus  23461  idnghm  24673  xmetdcn2  24766  pi1addval  24988  ipcau2  25175  gausslemma2dlem1a  27311  2lgs  27353  etasslt2  27760  uhgrsubgrself  29106  wlkl0  30190  mhmimasplusg  32771  lmhmimasvsca  32772  rlocaddval  32995  rlocmulval  32996  qusvsval  33077  qusmul  33127  carsgclctunlem2  33939  carsgclctun  33941  ballotlem1ri  34154  satefvfmla0  35028  satefvfmla1  35035  ftc1anclem5  37170  opoc1  38674  opoc0  38675  dochsat  40856  lcfrlem9  41023  pellfundex  42306  mnringmulrcld  43665  0ellimcdiv  45037  add2cncf  45290  stoweidlem21  45409  stoweidlem23  45411  stoweidlem32  45420  stoweidlem36  45424  stoweidlem40  45428  stoweidlem41  45429  natglobalincr  46263  mod42tp1mod8  46942  lincval0  47483

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »