Axiom ax-MP 14

Description: Rule of Modus Ponens.

Hypotheses

Ref	Expression
ax-MP.1	⊢ 𝜑
ax-MP.2	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ax-MP	⊢ 𝜓

Detailed syntax breakdown of Axiom ax-MP

Step	Hyp	Ref	Expression
1		wff-ps	1 wff 𝜓

This axiom is referenced by:  axL1.SH  30  axL2.SH  31  axL3.SH  32  mae-P1.1  33  syl-P1.2  34  id-P1.4  36  rae-P1.5.SH  38  rcp-FR1.SH  40  rcp-FR2.SH  42  rcp-FR3.SH  44  axL1.AC.SH  45  axL2.AC.SH  46  axL3.AC.SH  47  imcomm-P1.6.SH  49  imcomm-P1.6.AC.SH  50  imsubr-P1.7a.SH  52  imsubr-P1.7a.AC.SH  53  imsubl-P1.7b.SH  55  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.15a.SH  77  trnsp-P1.15b.AC.SH  79  trnsp-P1.15c.SH  81  trnsp-P1.15c.AC.SH  82  trnsp-P1.15d.AC.SH  84  trnsp-P1.15d.2AC.SH  85  pfbycont-P1.16.AC.2SH  87  pfbycase-P1.17.2SH  89  pfbycase-P1.17.AC.2SH  90  import-L2.1a.SH  92  export-L2.1b.SH  94  simpl-L2.2a.SH  96  simpr-L2.2b.SH  98  cmb-L2.3.2SH  100  dfbialt-P2.4  110  bifwd-P2.5a.SH  112  bifwd-P2.5a.AC.SH  113  bifwd-P2.5a.2AC.SH  114  birev-P2.5b.SH  116  birev-P2.5b.AC.SH  117  birev-P2.5b.2AC.SH  118  bicmb-P2.5c.2SH  120  bicmb-P2.5c.AC.2SH  121  bicmb-P2.5c.2AC.2SH  122  bisym-P2.6b.SH  125  subiml-P2.8a.SH  129  subimr-P2.8b.SH  131  simpl-P2.9a.AC.SH  135  simpr-P2.9b.AC.SH  137  cmb-P2.9c  138  cmb-P2.9c.AC.2SH  139  import-P2.10a.SH  141  export-P2.10b.SH  143  orintl-P2.11a.AC.SH  147  orintr-P2.11b.AC.SH  149  orelim-P2.11c.AC.3SH  151  true-P2.14  156  false-P2.15  159  ndtruee-P3.18  183  ndfalsee-P3.20  185  rcp-NDSEP3  186  rcp-NDSEP4  187  rcp-NDSEP5  188  rcp-NDJOIN3  189  rcp-NDJOIN4  190  rcp-NDJOIN5  191