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  10688  bcpasc  14244  sqreulem  15283  qnumdencoprm  16672  qeqnumdivden  16673  xpsaddlem  17494  xpsvsca  17498  xpsle  17500  grpinvid  18929  qus0  19118  ghmid  19151  lsm01  19600  frgpadd  19692  abvneg  20759  lsmcv  21096  qusmul2idl  21234  discmp  23342  kgenhaus  23488  idnghm  24687  xmetdcn2  24782  pi1addval  25004  ipcau2  25190  gausslemma2dlem1a  27332  2lgs  27374  etaslts2  27790  uhgrsubgrself  29353  wlkl0  30442  mhmimasplusg  33120  lmhmimasvsca  33121  rlocaddval  33350  rlocmulval  33351  qusvsval  33433  carsgclctunlem2  34476  carsgclctun  34478  ballotlem1ri  34692  satefvfmla0  35612  satefvfmla1  35619  ftc1anclem5  37894  opoc1  39458  opoc0  39459  dochsat  41639  lcfrlem9  41806  fisdomnn  42495  pellfundex  43124  mnringmulrcld  44465  0ellimcdiv  45889  add2cncf  46142  stoweidlem21  46261  stoweidlem23  46263  stoweidlem32  46272  stoweidlem36  46276  stoweidlem40  46280  stoweidlem41  46281  natglobalincr  47117  mod42tp1mod8  47844  cycldlenngric  48170  lincval0  48657