Theorem mpd3an23 1465

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 1373	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  10737  bcpasc  14293  sqreulem  15333  qnumdencoprm  16722  qeqnumdivden  16723  xpsaddlem  17543  xpsvsca  17547  xpsle  17549  grpinvid  18938  qus0  19128  ghmid  19161  lsm01  19608  frgpadd  19700  abvneg  20742  lsmcv  21058  qusmul2idl  21196  discmp  23292  kgenhaus  23438  idnghm  24638  xmetdcn2  24733  pi1addval  24955  ipcau2  25141  gausslemma2dlem1a  27283  2lgs  27325  etasslt2  27733  uhgrsubgrself  29214  wlkl0  30303  mhmimasplusg  32986  lmhmimasvsca  32987  rlocaddval  33226  rlocmulval  33227  qusvsval  33330  carsgclctunlem2  34317  carsgclctun  34319  ballotlem1ri  34533  satefvfmla0  35412  satefvfmla1  35419  ftc1anclem5  37698  opoc1  39202  opoc0  39203  dochsat  41384  lcfrlem9  41551  fisdomnn  42239  pellfundex  42881  mnringmulrcld  44224  0ellimcdiv  45654  add2cncf  45907  stoweidlem21  46026  stoweidlem23  46028  stoweidlem32  46037  stoweidlem36  46041  stoweidlem40  46045  stoweidlem41  46046  natglobalincr  46882  mod42tp1mod8  47607  cycldlenngric  47932  lincval0  48408