Theorem mpd3an23 1461

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  rankcf  10464  bcpasc  13963  sqreulem  14999  qnumdencoprm  16377  qeqnumdivden  16378  xpsaddlem  17201  xpsvsca  17205  xpsle  17207  grpinvid  18551  qus0  18729  ghmid  18755  lsm01  19192  frgpadd  19284  abvneg  20009  lsmcv  20318  discmp  22457  kgenhaus  22603  idnghm  23813  xmetdcn2  23906  pi1addval  24117  ipcau2  24303  gausslemma2dlem1a  26418  2lgs  26460  uhgrsubgrself  27550  wlkl0  28632  carsgclctunlem2  32186  carsgclctun  32188  ballotlem1ri  32401  satefvfmla0  33280  satefvfmla1  33287  etasslt2  33935  ftc1anclem5  35781  opoc1  37143  opoc0  37144  dochsat  39324  lcfrlem9  39491  pellfundex  40624  mnringmulrcld  41735  0ellimcdiv  43080  add2cncf  43333  stoweidlem21  43452  stoweidlem23  43454  stoweidlem32  43463  stoweidlem36  43467  stoweidlem40  43471  stoweidlem41  43472  mod42tp1mod8  44942  lincval0  45644