Theorem mpd3an23 1493

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 23	. 2 ⊢ (𝜑 → 𝜑)
2		mpd3an23.1	. 2 ⊢ (𝜑 → 𝜓)
3		mpd3an23.2	. 2 ⊢ (𝜑 → 𝜒)
4		mpd3an23.3	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
5	1, 2, 3, 4	syl3anc 1399	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  rankcf  10892  bcpasc  14495  sqreulem  15559  qnumdencoprm  16953  qeqnumdivden  16954  xpsaddlem  17777  xpsvsca  17781  xpsle  17783  grpinvid  19242  qus0  19436  ghmid  19468  lsm01  19918  frgpadd  20010  abvneg  21116  lsmcv  21452  qusmul2idl  21607  discmp  23749  kgenhaus  23896  idnghm  25095  xmetdcn2  25190  pi1addval  25402  ipcau2  25588  gausslemma2dlem1a  27725  2lgs  27767  etaslts2  28213  uhgrsubgrself  29894  wlkl0  31001  mhmimasplusg  33674  lmhmimasvsca  33675  rlocaddval  33906  rlocmulval  33907  qusvsval  33997  carsgclctunlem2  35034  carsgclctun  35036  ballotlem1ri  35250  satefvfmla0  36363  satefvfmla1  36370  ftc1anclem5  38820  opoc1  40462  opoc0  40463  dochsat  42643  lcfrlem9  42810  fisdomnn  43499  pellfundex  44097  mnringmulrcld  45429  0ellimcdiv  46874  add2cncf  47127  stoweidlem21  47246  stoweidlem23  47248  stoweidlem32  47257  stoweidlem36  47261  stoweidlem40  47265  stoweidlem41  47266  mod42tp1mod8  48902  cycldlenngric  49241  lincval0  49742