Theorem mpd3an23 1464

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  rankcf  10767  bcpasc  14276  sqreulem  15301  qnumdencoprm  16676  qeqnumdivden  16677  xpsaddlem  17514  xpsvsca  17518  xpsle  17520  grpinvid  18879  qus0  19061  ghmid  19091  lsm01  19531  frgpadd  19623  abvneg  20429  lsmcv  20741  qusmul2  20861  discmp  22883  kgenhaus  23029  idnghm  24241  xmetdcn2  24334  pi1addval  24545  ipcau2  24732  gausslemma2dlem1a  26847  2lgs  26889  etasslt2  27294  uhgrsubgrself  28516  wlkl0  29599  qusvsval  32435  qusmul  32479  carsgclctunlem2  33255  carsgclctun  33257  ballotlem1ri  33470  satefvfmla0  34346  satefvfmla1  34353  ftc1anclem5  36502  opoc1  38009  opoc0  38010  dochsat  40191  lcfrlem9  40358  pellfundex  41556  mnringmulrcld  42919  0ellimcdiv  44299  add2cncf  44552  stoweidlem21  44671  stoweidlem23  44673  stoweidlem32  44682  stoweidlem36  44686  stoweidlem40  44690  stoweidlem41  44691  natglobalincr  45525  mod42tp1mod8  46204  lincval0  46997