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

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  10790  bcpasc  14389  sqreulem  15451  qnumdencoprm  16842  qeqnumdivden  16843  xpsaddlem  17665  xpsvsca  17669  xpsle  17671  grpinvid  19129  qus0  19323  ghmid  19355  lsm01  19804  frgpadd  19896  abvneg  20998  lsmcv  21334  qusmul2idl  21487  discmp  23629  kgenhaus  23776  idnghm  24975  xmetdcn2  25070  pi1addval  25282  ipcau2  25468  gausslemma2dlem1a  27609  2lgs  27651  etaslts2  28067  uhgrsubgrself  29748  wlkl0  30855  mhmimasplusg  33485  lmhmimasvsca  33486  rlocaddval  33717  rlocmulval  33718  qusvsval  33800  carsgclctunlem2  34838  carsgclctun  34840  ballotlem1ri  35054  satefvfmla0  36005  satefvfmla1  36012  ftc1anclem5  38454  opoc1  40083  opoc0  40084  dochsat  42264  lcfrlem9  42431  fisdomnn  43119  pellfundex  43735  mnringmulrcld  45074  0ellimcdiv  46485  add2cncf  46738  stoweidlem21  46857  stoweidlem23  46859  stoweidlem32  46868  stoweidlem36  46872  stoweidlem40  46876  stoweidlem41  46877  mod42tp1mod8  48513  cycldlenngric  48852  lincval0  49353