Theorem axL1.SH 30

Description: Inference from ax-L1 11.

Hypothesis

Ref	Expression
axL1.SH.1	⊢ 𝜑

Assertion

Ref	Expression
axL1.SH	⊢ (𝜓 → 𝜑)

Proof of Theorem axL1.SH

Step	Hyp	Ref	Expression
1		axL1.SH.1	. 2 ⊢ 𝜑
2		ax-L1 11	. 2 ⊢ (𝜑 → (𝜓 → 𝜑))
3	1, 2	ax-MP 14	1 ⊢ (𝜓 → 𝜑)

Syntax hints:   → wff-imp 10

This theorem was proved from axioms:  ax-L1 11  ax-MP 14

This theorem is referenced by:  mae-P1.1  33  syl-P1.2  34  rcp-FR2  41  rcp-FR3  43  axL1.AC.SH  45  axL2.AC.SH  46  axL3.AC.SH  47  imcomm-P1.6.AC.SH  50  imsubr-P1.7a.AC.SH  53  imsubl-P1.7b.AC.SH  56  mpt-P1.8.AC.2SH  58  mpt-P1.8.2AC.2SH  59  mpt-P1.8.3AC.2SH  60  sylt-P1.9.AC.2SH  62  sylt-P1.9.2AC.2SH  63  poe-P1.11b.AC.2SH  67  clav-P1.12.AC.SH  69  clav-P1.12.2AC.SH  70  clav-P1.14.AC.SH  74  nclav-P1.14.2AC.SH  75  trnsp-P1.15b.AC.SH  79  trnsp-P1.15c.AC.SH  82  trnsp-P1.15d.AC.SH  84  trnsp-P1.15d.2AC.SH  85  pfbycont-P1.16  86  pfbycont-P1.16.AC.2SH  87  pfbycase-P1.17  88  pfbycase-P1.17.AC.2SH  90  import-L2.1a  91  simpr-L2.2b  97  bifwd-P2.5a.AC.SH  113  bifwd-P2.5a.2AC.SH  114  birev-P2.5b.AC.SH  117  birev-P2.5b.2AC.SH  118  bicmb-P2.5c  119  bicmb-P2.5c.AC.2SH  121  bicmb-P2.5c.2AC.2SH  122  bitrns-P2.6c  126  simpl-P2.9a.AC.SH  135  simpr-P2.9b.AC.SH  137  cmb-P2.9c.AC.2SH  139  import-P2.10a  140  export-P2.10b  142  orintl-P2.11a.AC.SH  147  orintr-P2.11b.AC.SH  149  orelim-P2.11c.AC.3SH  151  truejust-P2.13  154  ndtruei-P3.17  182