Theorem mpd3an23 1462

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  rankcf  10775  bcpasc  14286  sqreulem  15311  qnumdencoprm  16686  qeqnumdivden  16687  xpsaddlem  17524  xpsvsca  17528  xpsle  17530  grpinvid  18921  qus0  19105  ghmid  19137  lsm01  19581  frgpadd  19673  abvneg  20586  lsmcv  20900  qusmul2  21026  discmp  23123  kgenhaus  23269  idnghm  24481  xmetdcn2  24574  pi1addval  24796  ipcau2  24983  gausslemma2dlem1a  27101  2lgs  27143  etasslt2  27549  uhgrsubgrself  28801  wlkl0  29884  mhmimasplusg  32463  lmhmimasvsca  32464  qusvsval  32734  qusmul  32786  carsgclctunlem2  33613  carsgclctun  33615  ballotlem1ri  33828  satefvfmla0  34704  satefvfmla1  34711  ftc1anclem5  36869  opoc1  38376  opoc0  38377  dochsat  40558  lcfrlem9  40725  pellfundex  41927  mnringmulrcld  43290  0ellimcdiv  44665  add2cncf  44918  stoweidlem21  45037  stoweidlem23  45039  stoweidlem32  45048  stoweidlem36  45052  stoweidlem40  45056  stoweidlem41  45057  natglobalincr  45891  mod42tp1mod8  46570  lincval0  47185