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  10678  bcpasc  14238  sqreulem  15277  qnumdencoprm  16666  qeqnumdivden  16667  xpsaddlem  17487  xpsvsca  17491  xpsle  17493  grpinvid  18922  qus0  19111  ghmid  19144  lsm01  19593  frgpadd  19685  abvneg  20751  lsmcv  21088  qusmul2idl  21226  discmp  23323  kgenhaus  23469  idnghm  24668  xmetdcn2  24763  pi1addval  24985  ipcau2  25171  gausslemma2dlem1a  27313  2lgs  27355  etasslt2  27765  uhgrsubgrself  29269  wlkl0  30358  mhmimasplusg  33030  lmhmimasvsca  33031  rlocaddval  33246  rlocmulval  33247  qusvsval  33328  carsgclctunlem2  34343  carsgclctun  34345  ballotlem1ri  34559  satefvfmla0  35473  satefvfmla1  35480  ftc1anclem5  37747  opoc1  39311  opoc0  39312  dochsat  41492  lcfrlem9  41659  fisdomnn  42352  pellfundex  42993  mnringmulrcld  44335  0ellimcdiv  45761  add2cncf  46014  stoweidlem21  46133  stoweidlem23  46135  stoweidlem32  46144  stoweidlem36  46148  stoweidlem40  46152  stoweidlem41  46153  natglobalincr  46989  mod42tp1mod8  47716  cycldlenngric  48042  lincval0  48530