Theorem psubim-P6-L2 790

Description: Lemma for psubim-P6 791.

Assertion

Ref	Expression
psubim-P6-L2	⊢ (([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓) → [𝑡 / 𝑥](𝜑 → 𝜓))

Proof of Theorem psubim-P6-L2

Step	Hyp	Ref	Expression
1		impoe-P4.4a.CL 379	. . . . . 6 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
2	1	psubthm-P6 786	. . . . 5 ⊢ [𝑡 / 𝑥](¬ 𝜑 → (𝜑 → 𝜓))
3		psubim-P6-L1 789	. . . . 5 ⊢ ([𝑡 / 𝑥](¬ 𝜑 → (𝜑 → 𝜓)) → ([𝑡 / 𝑥] ¬ 𝜑 → [𝑡 / 𝑥](𝜑 → 𝜓)))
4	2, 3	rcp-NDIME0 228	. . . 4 ⊢ ([𝑡 / 𝑥] ¬ 𝜑 → [𝑡 / 𝑥](𝜑 → 𝜓))
5		psubneg-P6 788	. . . 4 ⊢ ([𝑡 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑡 / 𝑥]𝜑)
6	4, 5	subiml2-P4.RC 541	. . 3 ⊢ (¬ [𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥](𝜑 → 𝜓))
7		axL1-P3.21.CL 253	. . . . 5 ⊢ (𝜓 → (𝜑 → 𝜓))
8	7	psubthm-P6 786	. . . 4 ⊢ [𝑡 / 𝑥](𝜓 → (𝜑 → 𝜓))
9		psubim-P6-L1 789	. . . 4 ⊢ ([𝑡 / 𝑥](𝜓 → (𝜑 → 𝜓)) → ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥](𝜑 → 𝜓)))
10	8, 9	rcp-NDIME0 228	. . 3 ⊢ ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥](𝜑 → 𝜓))
11	6, 10	joinimandinc3-P4.RC 579	. 2 ⊢ ((¬ [𝑡 / 𝑥]𝜑 ∨ [𝑡 / 𝑥]𝜓) → [𝑡 / 𝑥](𝜑 → 𝜓))
12		imasor-P4.32a 487	. . 3 ⊢ (([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓) ↔ (¬ [𝑡 / 𝑥]𝜑 ∨ [𝑡 / 𝑥]𝜓))
13	12	bisym-P3.33b.RC 299	. 2 ⊢ ((¬ [𝑡 / 𝑥]𝜑 ∨ [𝑡 / 𝑥]𝜓) ↔ ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓))
14	11, 13	subiml2-P4.RC 541	1 ⊢ (([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓) → [𝑡 / 𝑥](𝜑 → 𝜓))

Syntax hints:  ¬ wff-neg 9   → wff-imp 10   ∨ wff-or 144  [wff-psub 714

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18  ax-L7 19  ax-L10 27  ax-L12 29

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  df-exists-D5.1 596  df-nfree-D6.1 682  df-psub-D6.2 716

This theorem is referenced by:  psubim-P6  791