Theorem axL1-P3.21 252

Description: Re-derived Deductive Form of Axiom L1. †

Hypothesis

Ref	Expression
axL1-P3.21.1	⊢ (𝛾 → 𝜑)

Assertion

Ref	Expression
axL1-P3.21	⊢ (𝛾 → (𝜓 → 𝜑))

Proof of Theorem axL1-P3.21

Step	Hyp	Ref	Expression
1		axL1-P3.21.1	. . 3 ⊢ (𝛾 → 𝜑)
2	1	rcp-NDIMP1add1 208	. 2 ⊢ ((𝛾 ∧ 𝜓) → 𝜑)
3	2	rcp-NDIMI2 224	1 ⊢ (𝛾 → (𝜓 → 𝜑))

Syntax hints:   → wff-imp 10

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

This theorem is referenced by:  axL1-P3.21.CL  253  andasim-P3.46-L2  355  sepimorr-P4.9c  412  sepimandl-P4.9d  415  imoverim-P4.30-L1  476  imasor-P4.32-L2  486  biasandorint-P4.34b  492  specpsub-P6  721  qimeqex-P7-L1  1054  nfrcond-P8  1108