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

Syntax hints:   → wi 4   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  rankcf  10237  bcpasc  13731  sqreulem  14767  qnumdencoprm  16140  qeqnumdivden  16141  xpsaddlem  16904  xpsvsca  16908  xpsle  16910  grpinvid  18227  qus0  18405  ghmid  18431  lsm01  18864  frgpadd  18956  abvneg  19673  lsmcv  19981  discmp  22098  kgenhaus  22244  idnghm  23445  xmetdcn2  23538  pi1addval  23749  ipcau2  23934  gausslemma2dlem1a  26048  2lgs  26090  uhgrsubgrself  27169  wlkl0  28251  carsgclctunlem2  31805  carsgclctun  31807  ballotlem1ri  32020  satefvfmla0  32896  satefvfmla1  32903  etasslt2  33569  ftc1anclem5  35414  opoc1  36778  opoc0  36779  dochsat  38959  lcfrlem9  39126  pellfundex  40200  mnringmulrcld  41309  0ellimcdiv  42657  add2cncf  42910  stoweidlem21  43029  stoweidlem23  43031  stoweidlem32  43040  stoweidlem36  43044  stoweidlem40  43048  stoweidlem41  43049  mod42tp1mod8  44487  lincval0  45189