Theorem mpd3an23 1465

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 1373	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  rankcf  10668  bcpasc  14228  sqreulem  15267  qnumdencoprm  16656  qeqnumdivden  16657  xpsaddlem  17477  xpsvsca  17481  xpsle  17483  grpinvid  18912  qus0  19102  ghmid  19135  lsm01  19584  frgpadd  19676  abvneg  20742  lsmcv  21079  qusmul2idl  21217  discmp  23314  kgenhaus  23460  idnghm  24659  xmetdcn2  24754  pi1addval  24976  ipcau2  25162  gausslemma2dlem1a  27304  2lgs  27346  etasslt2  27756  uhgrsubgrself  29259  wlkl0  30345  mhmimasplusg  33017  lmhmimasvsca  33018  rlocaddval  33233  rlocmulval  33234  qusvsval  33315  carsgclctunlem2  34330  carsgclctun  34332  ballotlem1ri  34546  satefvfmla0  35460  satefvfmla1  35467  ftc1anclem5  37743  opoc1  39247  opoc0  39248  dochsat  41428  lcfrlem9  41595  fisdomnn  42283  pellfundex  42925  mnringmulrcld  44267  0ellimcdiv  45693  add2cncf  45946  stoweidlem21  46065  stoweidlem23  46067  stoweidlem32  46076  stoweidlem36  46080  stoweidlem40  46084  stoweidlem41  46085  natglobalincr  46921  mod42tp1mod8  47639  cycldlenngric  47965  lincval0  48453