a1d - Metamath Proof Explorer a1d - Intuitionistic Logic Explorer Hypothesis Ref Expression a1d.1 ⊢(𝜑→𝜓) Assertion Ref Expression a1d ⊢(𝜑→(𝜒→𝜓)) Proof of Theorem a1d Step Hyp Ref Expression 1 ax-1 ⊢(𝜓→(𝜒→𝜓)) 2 ax-1 ⊢( (𝜓→(𝜒→𝜓)) → (𝜑→(𝜓→(𝜒→…