Theorem syl-P3.24.RC 260

Description: Inference Form of syl-P3.24.RC 260. †

Hypotheses

Ref	Expression
syl-P3.24.RC.1	⊢ (𝜑 → 𝜓)
syl-P3.24.RC.2	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
syl-P3.24.RC	⊢ (𝜑 → 𝜒)

Proof of Theorem syl-P3.24.RC

Step	Hyp	Ref	Expression
1		syl-P3.24.RC.1	. . . 4 ⊢ (𝜑 → 𝜓)
2	1	ndtruei-P3.17 182	. . 3 ⊢ (⊤ → (𝜑 → 𝜓))
3		syl-P3.24.RC.2	. . . 4 ⊢ (𝜓 → 𝜒)
4	3	ndtruei-P3.17 182	. . 3 ⊢ (⊤ → (𝜓 → 𝜒))
5	2, 4	syl-P3.24 259	. 2 ⊢ (⊤ → (𝜑 → 𝜒))
6	5	ndtruee-P3.18 183	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wff-imp 10  ⊤wff-true 153

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-true-D2.4 155

This theorem is referenced by:  oroverbiint-P4.28d  471  imoverand-P4.29a  472  imoveror-P4.29-L1  473  rimoverand-P4.31-L1  480  rimoveror-P4.31b  482  allicv-P5  614  exiav-P5  615  subeqr-P5  635  subelofl-P5  638  subelofr-P5  640  subsucc-P5  644  subaddl-P5  645  subaddr-P5  646  submultl-P5  649  submultr-P5  650  lemma-L5.02a  653  cbvallv-P5-L1  658  specw-P5  661  nfrgenw-P6  684  gennfrw-P6  685  nfrall2w-P6  694  nfrex2w-P6  695  trnsvsubw-P6  710  qremall-P6  722  qremex-P6  723  nfrgen-P6  733  gennfr-P6  734  nfrall2-P6  743  nfrex2-P6  744  allic-P6  745  exia-P6  746  lemma-L6.04a  749  trnsvsub-P6  763  spliteq-P6-L1  775  exgennfrcl-L6  814  nfrall2d-P6  819  nfrex2d-P6  820  ndalle-P7.18  843  ndexi-P7.19  844  alli-P7  947  alloverimex-P7  948  dfexistsint-P7  960  dfnfreealtif-P7  964  alloverim-P7  970  qimeqallb-P7  976  qimeqalla-P7  1050  cbvall-P7-L1  1060  cbvex-P7-L1  1065  exallnfr-P8  1092  nfrcond-P8  1108