Theorem mpd3an23 1462

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

Syntax hints:   → wi 4   ∧ w3a 1086

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

This theorem is referenced by:  rankcf  10815  bcpasc  14357  sqreulem  15395  qnumdencoprm  16779  qeqnumdivden  16780  xpsaddlem  17620  xpsvsca  17624  xpsle  17626  grpinvid  19030  qus0  19220  ghmid  19253  lsm01  19704  frgpadd  19796  abvneg  20844  lsmcv  21161  qusmul2idl  21307  discmp  23422  kgenhaus  23568  idnghm  24780  xmetdcn2  24873  pi1addval  25095  ipcau2  25282  gausslemma2dlem1a  27424  2lgs  27466  etasslt2  27874  uhgrsubgrself  29312  wlkl0  30396  mhmimasplusg  33026  lmhmimasvsca  33027  rlocaddval  33255  rlocmulval  33256  qusvsval  33360  carsgclctunlem2  34301  carsgclctun  34303  ballotlem1ri  34516  satefvfmla0  35403  satefvfmla1  35410  ftc1anclem5  37684  opoc1  39184  opoc0  39185  dochsat  41366  lcfrlem9  41533  fisdomnn  42264  pellfundex  42874  mnringmulrcld  44224  0ellimcdiv  45605  add2cncf  45858  stoweidlem21  45977  stoweidlem23  45979  stoweidlem32  45988  stoweidlem36  45992  stoweidlem40  45996  stoweidlem41  45997  natglobalincr  46831  mod42tp1mod8  47527  lincval0  48261