Theorem mpd3an23 1487

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  rankcf  10750  bcpasc  14348  sqreulem  15401  qnumdencoprm  16794  qeqnumdivden  16795  xpsaddlem  17617  xpsvsca  17621  xpsle  17623  grpinvid  19056  qus0  19251  ghmid  19283  lsm01  19732  frgpadd  19824  abvneg  20898  lsmcv  21234  qusmul2idl  21380  discmp  23516  kgenhaus  23662  idnghm  24861  xmetdcn2  24956  pi1addval  25168  ipcau2  25354  gausslemma2dlem1a  27487  2lgs  27529  etaslts2  27945  uhgrsubgrself  29539  wlkl0  30627  mhmimasplusg  33270  lmhmimasvsca  33271  rlocaddval  33502  rlocmulval  33503  qusvsval  33587  carsgclctunlem2  34626  carsgclctun  34628  ballotlem1ri  34842  satefvfmla0  35781  satefvfmla1  35788  ftc1anclem5  38208  opoc1  39838  opoc0  39839  dochsat  42019  lcfrlem9  42186  fisdomnn  42872  pellfundex  43475  mnringmulrcld  44816  0ellimcdiv  46221  add2cncf  46474  stoweidlem21  46593  stoweidlem23  46595  stoweidlem32  46604  stoweidlem36  46608  stoweidlem40  46612  stoweidlem41  46613  natglobalincr  47451  mod42tp1mod8  48209  cycldlenngric  48548  lincval0  49046