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  10862  bcpasc  14465  sqreulem  15527  qnumdencoprm  16921  qeqnumdivden  16922  xpsaddlem  17745  xpsvsca  17749  xpsle  17751  grpinvid  19210  qus0  19404  ghmid  19436  lsm01  19885  frgpadd  19977  abvneg  21083  lsmcv  21419  qusmul2idl  21574  discmp  23716  kgenhaus  23863  idnghm  25062  xmetdcn2  25157  pi1addval  25369  ipcau2  25555  gausslemma2dlem1a  27692  2lgs  27734  etaslts2  28180  uhgrsubgrself  29861  wlkl0  30968  mhmimasplusg  33598  lmhmimasvsca  33599  rlocaddval  33830  rlocmulval  33831  qusvsval  33913  carsgclctunlem2  34951  carsgclctun  34953  ballotlem1ri  35167  satefvfmla0  36183  satefvfmla1  36190  ftc1anclem5  38616  opoc1  40260  opoc0  40261  dochsat  42441  lcfrlem9  42608  fisdomnn  43296  pellfundex  43893  mnringmulrcld  45226  0ellimcdiv  46659  add2cncf  46912  stoweidlem21  47031  stoweidlem23  47033  stoweidlem32  47042  stoweidlem36  47046  stoweidlem40  47050  stoweidlem41  47051  mod42tp1mod8  48687  cycldlenngric  49026  lincval0  49527