Axiom ax-L1 11

Description: Axiom of Simplification.

Assertion

Ref	Expression
ax-L1	⊢ (𝜑 → (𝜓 → 𝜑))

Detailed syntax breakdown of Axiom ax-L1

Step	Hyp	Ref	Expression
1		wff-ph	. 2 wff 𝜑
2		wff-ps	. . 3 wff 𝜓
3	2, 1	wff-imp 10	. 2 wff (𝜓 → 𝜑)
4	1, 3	wff-imp 10	1 wff (𝜑 → (𝜓 → 𝜑))

This axiom is referenced by:  axL1.SH  30  id-P1.4  36  axL1.AC.SH  45  imcomm-P1.6  48  imsubr-P1.7a  51  poe-P1.11a  65  pfbycont-P1.16  86  pfbycase-P1.17  88  simpl-L2.2a  95  bitrns-P2.6c  126  import-P2.10a  140  export-P2.10b  142