Theorem mpd3an23 1426

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

Syntax hints:   → wi 4   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  rankcf  9599  bcpasc  13108  sqreulem  14099  qnumdencoprm  15453  qeqnumdivden  15454  xpsaddlem  16235  xpsvsca  16239  xpsle  16241  grpinvid  17476  qus0  17652  ghmid  17666  lsm01  18084  frgpadd  18176  abvneg  18834  lsmcv  19141  discmp  21201  kgenhaus  21347  idnghm  22547  xmetdcn2  22640  pi1addval  22848  ipcau2  23033  gausslemma2dlem1a  25090  2lgs  25132  uhgrsubgrself  26172  carsgclctunlem2  30381  carsgclctun  30383  ballotlem1ri  30596  ftc1anclem5  33489  opoc1  34489  opoc0  34490  dochsat  36672  lcfrlem9  36839  pellfundex  37450  0ellimcdiv  39881  add2cncf  40116  stoweidlem21  40238  stoweidlem23  40240  stoweidlem32  40249  stoweidlem36  40253  stoweidlem40  40257  stoweidlem41  40258  mod42tp1mod8  41519  lincval0  42204