Theorem mpd3an23 1483

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  rankcf  10732  bcpasc  14331  sqreulem  15370  qnumdencoprm  16763  qeqnumdivden  16764  xpsaddlem  17586  xpsvsca  17590  xpsle  17592  grpinvid  19024  qus0  19213  ghmid  19245  lsm01  19694  frgpadd  19786  abvneg  20855  lsmcv  21191  qusmul2idl  21329  discmp  23438  kgenhaus  23584  idnghm  24783  xmetdcn2  24878  pi1addval  25090  ipcau2  25276  gausslemma2dlem1a  27406  2lgs  27448  etaslts2  27864  uhgrsubgrself  29427  wlkl0  30515  mhmimasplusg  33177  lmhmimasvsca  33178  rlocaddval  33411  rlocmulval  33412  qusvsval  33499  carsgclctunlem2  34577  carsgclctun  34579  ballotlem1ri  34793  satefvfmla0  35732  satefvfmla1  35739  ftc1anclem5  38160  opoc1  39790  opoc0  39791  dochsat  41971  lcfrlem9  42138  fisdomnn  42824  pellfundex  43427  mnringmulrcld  44768  0ellimcdiv  46187  add2cncf  46440  stoweidlem21  46559  stoweidlem23  46561  stoweidlem32  46570  stoweidlem36  46574  stoweidlem40  46578  stoweidlem41  46579  natglobalincr  47417  mod42tp1mod8  48175  cycldlenngric  48514  lincval0  49001