Theorem mpd3an23 1492

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 23	. 2 ⊢ (𝜑 → 𝜑)
2		mpd3an23.1	. 2 ⊢ (𝜑 → 𝜓)
3		mpd3an23.2	. 2 ⊢ (𝜑 → 𝜒)
4		mpd3an23.3	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
5	1, 2, 3, 4	syl3anc 1398	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  rankcf  10843  bcpasc  14445  sqreulem  15507  qnumdencoprm  16901  qeqnumdivden  16902  xpsaddlem  17725  xpsvsca  17729  xpsle  17731  grpinvid  19190  qus0  19384  ghmid  19416  lsm01  19865  frgpadd  19957  abvneg  21063  lsmcv  21399  qusmul2idl  21554  discmp  23696  kgenhaus  23843  idnghm  25042  xmetdcn2  25137  pi1addval  25349  ipcau2  25535  gausslemma2dlem1a  27674  2lgs  27716  etaslts2  28162  uhgrsubgrself  29843  wlkl0  30950  mhmimasplusg  33580  lmhmimasvsca  33581  rlocaddval  33812  rlocmulval  33813  qusvsval  33895  carsgclctunlem2  34934  carsgclctun  34936  ballotlem1ri  35150  satefvfmla0  36152  satefvfmla1  36159  ftc1anclem5  38583  opoc1  40227  opoc0  40228  dochsat  42408  lcfrlem9  42575  fisdomnn  43263  pellfundex  43846  mnringmulrcld  45185  0ellimcdiv  46603  add2cncf  46856  stoweidlem21  46975  stoweidlem23  46977  stoweidlem32  46986  stoweidlem36  46990  stoweidlem40  46994  stoweidlem41  46995  mod42tp1mod8  48631  cycldlenngric  48970  lincval0  49471