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  10780  bcpasc  14377  sqreulem  15437  qnumdencoprm  16829  qeqnumdivden  16830  xpsaddlem  17652  xpsvsca  17656  xpsle  17658  grpinvid  19097  qus0  19291  ghmid  19323  lsm01  19772  frgpadd  19864  abvneg  20966  lsmcv  21302  qusmul2idl  21455  discmp  23592  kgenhaus  23738  idnghm  24937  xmetdcn2  25032  pi1addval  25244  ipcau2  25430  gausslemma2dlem1a  27566  2lgs  27608  etaslts2  28024  uhgrsubgrself  29667  wlkl0  30755  mhmimasplusg  33388  lmhmimasvsca  33389  rlocaddval  33620  rlocmulval  33621  qusvsval  33703  carsgclctunlem2  34741  carsgclctun  34743  ballotlem1ri  34957  satefvfmla0  35931  satefvfmla1  35938  ftc1anclem5  38389  opoc1  40017  opoc0  40018  dochsat  42198  lcfrlem9  42365  fisdomnn  43053  pellfundex  43654  mnringmulrcld  44993  0ellimcdiv  46404  add2cncf  46657  stoweidlem21  46776  stoweidlem23  46778  stoweidlem32  46787  stoweidlem36  46791  stoweidlem40  46795  stoweidlem41  46796  natglobalincr  47634  mod42tp1mod8  48395  cycldlenngric  48734  lincval0  49236