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  10690  bcpasc  14246  sqreulem  15285  qnumdencoprm  16674  qeqnumdivden  16675  xpsaddlem  17495  xpsvsca  17499  xpsle  17501  grpinvid  18896  qus0  19086  ghmid  19119  lsm01  19568  frgpadd  19660  abvneg  20729  lsmcv  21066  qusmul2idl  21204  discmp  23301  kgenhaus  23447  idnghm  24647  xmetdcn2  24742  pi1addval  24964  ipcau2  25150  gausslemma2dlem1a  27292  2lgs  27334  etasslt2  27743  uhgrsubgrself  29243  wlkl0  30329  mhmimasplusg  33005  lmhmimasvsca  33006  rlocaddval  33218  rlocmulval  33219  qusvsval  33299  carsgclctunlem2  34286  carsgclctun  34288  ballotlem1ri  34502  satefvfmla0  35390  satefvfmla1  35397  ftc1anclem5  37676  opoc1  39180  opoc0  39181  dochsat  41362  lcfrlem9  41529  fisdomnn  42217  pellfundex  42859  mnringmulrcld  44201  0ellimcdiv  45631  add2cncf  45884  stoweidlem21  46003  stoweidlem23  46005  stoweidlem32  46014  stoweidlem36  46018  stoweidlem40  46022  stoweidlem41  46023  natglobalincr  46859  mod42tp1mod8  47587  cycldlenngric  47913  lincval0  48401