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  10772  bcpasc  14281  sqreulem  15306  qnumdencoprm  16681  qeqnumdivden  16682  xpsaddlem  17519  xpsvsca  17523  xpsle  17525  grpinvid  18884  qus0  19068  ghmid  19098  lsm01  19539  frgpadd  19631  abvneg  20442  lsmcv  20754  qusmul2  20875  discmp  22902  kgenhaus  23048  idnghm  24260  xmetdcn2  24353  pi1addval  24564  ipcau2  24751  gausslemma2dlem1a  26868  2lgs  26910  etasslt2  27315  uhgrsubgrself  28537  wlkl0  29620  qusvsval  32467  qusmul  32515  carsgclctunlem2  33318  carsgclctun  33320  ballotlem1ri  33533  satefvfmla0  34409  satefvfmla1  34416  ftc1anclem5  36565  opoc1  38072  opoc0  38073  dochsat  40254  lcfrlem9  40421  pellfundex  41624  mnringmulrcld  42987  0ellimcdiv  44365  add2cncf  44618  stoweidlem21  44737  stoweidlem23  44739  stoweidlem32  44748  stoweidlem36  44752  stoweidlem40  44756  stoweidlem41  44757  natglobalincr  45591  mod42tp1mod8  46270  lincval0  47096