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  10730  bcpasc  14286  sqreulem  15326  qnumdencoprm  16715  qeqnumdivden  16716  xpsaddlem  17536  xpsvsca  17540  xpsle  17542  grpinvid  18931  qus0  19121  ghmid  19154  lsm01  19601  frgpadd  19693  abvneg  20735  lsmcv  21051  qusmul2idl  21189  discmp  23285  kgenhaus  23431  idnghm  24631  xmetdcn2  24726  pi1addval  24948  ipcau2  25134  gausslemma2dlem1a  27276  2lgs  27318  etasslt2  27726  uhgrsubgrself  29207  wlkl0  30296  mhmimasplusg  32979  lmhmimasvsca  32980  rlocaddval  33219  rlocmulval  33220  qusvsval  33323  carsgclctunlem2  34310  carsgclctun  34312  ballotlem1ri  34526  satefvfmla0  35405  satefvfmla1  35412  ftc1anclem5  37691  opoc1  39195  opoc0  39196  dochsat  41377  lcfrlem9  41544  fisdomnn  42232  pellfundex  42874  mnringmulrcld  44217  0ellimcdiv  45647  add2cncf  45900  stoweidlem21  46019  stoweidlem23  46021  stoweidlem32  46030  stoweidlem36  46034  stoweidlem40  46038  stoweidlem41  46039  natglobalincr  46875  mod42tp1mod8  47603  cycldlenngric  47928  lincval0  48404