Theorem subimr-P3.40b.RC 328

Description: Inference Form of subimr-P3.40b 327. †

Hypothesis

Ref	Expression
subimr-P3.40b.RC.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
subimr-P3.40b.RC	⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))

Proof of Theorem subimr-P3.40b.RC

Step	Hyp	Ref	Expression
1		subimr-P3.40b.RC.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	ndtruei-P3.17 182	. . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓))
3	2	subimr-P3.40b 327	. 2 ⊢ (⊤ → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)))
4	3	ndtruee-P3.18 183	1 ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))

Syntax hints:   → wff-imp 10   ↔ wff-bi 104  ⊤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:  oroverim-P4.28-L1  465  imoverbi-P4.30-L2  478  rimoverand-P4.31-L1  480  rimoveror-P4.31b  482  qcallimlv-P5  673  qceximlv-P5  674  solvedsub-P6a  711  lemma-L6.03a  728  qcalliml-P6  759  qceximl-P6  760  qcexandr-P6  761  lemma-L6.08a  773  psubleq-P6  783  psubnfr-P6  784  psubneg-P6  788  psuband-P6  792  nfrall2d-P6  819  ndexe-P6  825  dfpsub-P7  978  axL12-P7  982  qcalliml-P8  1124  qceximl-P8  1125