Theorem mpd3an23 1492

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

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  rankcf  10763  bcpasc  14359  sqreulem  15413  qnumdencoprm  16805  qeqnumdivden  16806  xpsaddlem  17628  xpsvsca  17632  xpsle  17634  grpinvid  19067  qus0  19261  ghmid  19293  lsm01  19742  frgpadd  19834  abvneg  20910  lsmcv  21246  qusmul2idl  21399  discmp  23536  kgenhaus  23682  idnghm  24881  xmetdcn2  24976  pi1addval  25188  ipcau2  25374  gausslemma2dlem1a  27510  2lgs  27552  etaslts2  27968  uhgrsubgrself  29611  wlkl0  30699  mhmimasplusg  33338  lmhmimasvsca  33339  rlocaddval  33570  rlocmulval  33571  qusvsval  33653  carsgclctunlem2  34690  carsgclctun  34692  ballotlem1ri  34906  satefvfmla0  35891  satefvfmla1  35898  ftc1anclem5  38329  opoc1  39957  opoc0  39958  dochsat  42138  lcfrlem9  42305  fisdomnn  42993  pellfundex  43596  mnringmulrcld  44935  0ellimcdiv  46346  add2cncf  46599  stoweidlem21  46718  stoweidlem23  46720  stoweidlem32  46729  stoweidlem36  46733  stoweidlem40  46737  stoweidlem41  46738  natglobalincr  47576  mod42tp1mod8  48337  cycldlenngric  48676  lincval0  49178