Theorem subiml-P3.40a.RC 326

Description: Inference Form of subiml-P3.40a 325. †

Hypothesis

Ref	Expression
subiml-P3.40a.RC.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
subiml-P3.40a.RC	⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

Proof of Theorem subiml-P3.40a.RC

Step	Hyp	Ref	Expression
1		subiml-P3.40a.RC.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	ndtruei-P3.17 182	. . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓))
3	2	subiml-P3.40a 325	. 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  imoverand-P4.29a  472  imoveror-P4.29-L1  473  peirce2exclmid-P4.41b  513  lemma-L5.01a  600  qcallimrv-P5  671  qceximrv-P5  672  qcallimr-P6  757  qceximr-P6  758  nfrexgencl-L6  813  nfrex2d-P6  820  qcallimr-P8  1122  qceximr-P8  1123