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  10865  bcpasc  14468  sqreulem  15532  qnumdencoprm  16926  qeqnumdivden  16927  xpsaddlem  17750  xpsvsca  17754  xpsle  17756  grpinvid  19215  qus0  19409  ghmid  19441  lsm01  19890  frgpadd  19982  abvneg  21088  lsmcv  21424  qusmul2idl  21579  discmp  23721  kgenhaus  23868  idnghm  25067  xmetdcn2  25162  pi1addval  25374  ipcau2  25560  gausslemma2dlem1a  27697  2lgs  27739  etaslts2  28185  uhgrsubgrself  29866  wlkl0  30973  mhmimasplusg  33644  lmhmimasvsca  33645  rlocaddval  33876  rlocmulval  33877  qusvsval  33959  carsgclctunlem2  34997  carsgclctun  34999  ballotlem1ri  35213  satefvfmla0  36269  satefvfmla1  36276  ftc1anclem5  38708  opoc1  40352  opoc0  40353  dochsat  42533  lcfrlem9  42700  fisdomnn  43388  pellfundex  43986  mnringmulrcld  45319  0ellimcdiv  46752  add2cncf  47005  stoweidlem21  47124  stoweidlem23  47126  stoweidlem32  47135  stoweidlem36  47139  stoweidlem40  47143  stoweidlem41  47144  mod42tp1mod8  48780  cycldlenngric  49119  lincval0  49620