Theorem subord-P3.43c 350

Description: Dual Substitution Theorem for '∨' . †

Hypotheses

Ref	Expression
subord-P3.43c.1	⊢ (𝛾 → (𝜑 ↔ 𝜓))
subord-P3.43c.2	⊢ (𝛾 → (𝜒 ↔ 𝜗))

Assertion

Ref	Expression
subord-P3.43c	⊢ (𝛾 → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜗)))

Proof of Theorem subord-P3.43c

Step	Hyp	Ref	Expression
1		subord-P3.43c.1	. . 3 ⊢ (𝛾 → (𝜑 ↔ 𝜓))
2	1	suborl-P3.43a 346	. 2 ⊢ (𝛾 → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)))
3		subord-P3.43c.2	. . 3 ⊢ (𝛾 → (𝜒 ↔ 𝜗))
4	3	suborr-P3.43b 348	. 2 ⊢ (𝛾 → ((𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜗)))
5	2, 4	bitrns-P3.33c 302	1 ⊢ (𝛾 → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜗)))

Syntax hints:   → wff-imp 10   ↔ wff-bi 104   ∨ wff-or 144

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-or-D2.3 145  df-true-D2.4 155  df-rcp-AND3 161

This theorem is referenced by:  subord-P3.43c.RC  351  subord2-P4  562  example-E5.02a  664