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  10791  bcpasc  14339  sqreulem  15378  qnumdencoprm  16764  qeqnumdivden  16765  xpsaddlem  17587  xpsvsca  17591  xpsle  17593  grpinvid  18982  qus0  19172  ghmid  19205  lsm01  19652  frgpadd  19744  abvneg  20786  lsmcv  21102  qusmul2idl  21240  discmp  23336  kgenhaus  23482  idnghm  24682  xmetdcn2  24777  pi1addval  24999  ipcau2  25186  gausslemma2dlem1a  27328  2lgs  27370  etasslt2  27778  uhgrsubgrself  29259  wlkl0  30348  mhmimasplusg  33033  lmhmimasvsca  33034  rlocaddval  33263  rlocmulval  33264  qusvsval  33367  carsgclctunlem2  34351  carsgclctun  34353  ballotlem1ri  34567  satefvfmla0  35440  satefvfmla1  35447  ftc1anclem5  37721  opoc1  39220  opoc0  39221  dochsat  41402  lcfrlem9  41569  fisdomnn  42295  pellfundex  42909  mnringmulrcld  44252  0ellimcdiv  45678  add2cncf  45931  stoweidlem21  46050  stoweidlem23  46052  stoweidlem32  46061  stoweidlem36  46065  stoweidlem40  46069  stoweidlem41  46070  natglobalincr  46906  mod42tp1mod8  47616  cycldlenngric  47941  lincval0  48391