Theorem mpd3an23 1466

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 1374	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  rankcf  10700  bcpasc  14283  sqreulem  15322  qnumdencoprm  16715  qeqnumdivden  16716  xpsaddlem  17537  xpsvsca  17541  xpsle  17543  grpinvid  18975  qus0  19164  ghmid  19197  lsm01  19646  frgpadd  19738  abvneg  20803  lsmcv  21139  qusmul2idl  21277  discmp  23363  kgenhaus  23509  idnghm  24708  xmetdcn2  24803  pi1addval  25015  ipcau2  25201  gausslemma2dlem1a  27328  2lgs  27370  etaslts2  27786  uhgrsubgrself  29349  wlkl0  30437  mhmimasplusg  33098  lmhmimasvsca  33099  rlocaddval  33329  rlocmulval  33330  qusvsval  33412  carsgclctunlem2  34463  carsgclctun  34465  ballotlem1ri  34679  satefvfmla0  35600  satefvfmla1  35607  ftc1anclem5  38018  opoc1  39648  opoc0  39649  dochsat  41829  lcfrlem9  41996  fisdomnn  42683  pellfundex  43314  mnringmulrcld  44655  0ellimcdiv  46077  add2cncf  46330  stoweidlem21  46449  stoweidlem23  46451  stoweidlem32  46460  stoweidlem36  46464  stoweidlem40  46468  stoweidlem41  46469  natglobalincr  47307  mod42tp1mod8  48065  cycldlenngric  48404  lincval0  48891