Theorem mpd3an23 1471

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  rankcf  10698  bcpasc  14281  sqreulem  15320  qnumdencoprm  16713  qeqnumdivden  16714  xpsaddlem  17535  xpsvsca  17539  xpsle  17541  grpinvid  18973  qus0  19162  ghmid  19195  lsm01  19644  frgpadd  19736  abvneg  20805  lsmcv  21141  qusmul2idl  21279  discmp  23388  kgenhaus  23534  idnghm  24733  xmetdcn2  24828  pi1addval  25040  ipcau2  25226  gausslemma2dlem1a  27353  2lgs  27395  etaslts2  27811  uhgrsubgrself  29374  wlkl0  30462  mhmimasplusg  33124  lmhmimasvsca  33125  rlocaddval  33356  rlocmulval  33357  qusvsval  33442  carsgclctunlem2  34510  carsgclctun  34512  ballotlem1ri  34726  satefvfmla0  35653  satefvfmla1  35660  ftc1anclem5  38071  opoc1  39701  opoc0  39702  dochsat  41882  lcfrlem9  42049  fisdomnn  42735  pellfundex  43338  mnringmulrcld  44679  0ellimcdiv  46099  add2cncf  46352  stoweidlem21  46471  stoweidlem23  46473  stoweidlem32  46482  stoweidlem36  46486  stoweidlem40  46490  stoweidlem41  46491  natglobalincr  47329  mod42tp1mod8  48087  cycldlenngric  48426  lincval0  48913