Theorem ndtruee-P3.18 183

Description: Natural Deduction: '⊤' Elimination Rule.

Rules 17 and 18 allow us to write '(⊤ → 𝜑)' as a synonym for stating "'𝜑' is true" (or, more precisely, deducable).

Hypothesis

Ref	Expression
ndtruee-P3.18.1	⊢ (⊤ → 𝜑)

Assertion

Ref	Expression
ndtruee-P3.18	⊢ 𝜑

Proof of Theorem ndtruee-P3.18

Step	Hyp	Ref	Expression
1		true-P2.14 156	. 2 ⊢ ⊤
2		ndtruee-P3.18.1	. 2 ⊢ (⊤ → 𝜑)
3	1, 2	ax-MP 14	1 ⊢ 𝜑

Syntax hints:   → wff-imp 10  ⊤wff-true 153

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-true-D2.4 155

This theorem is referenced by:  ndfalsei-P3.19  184  rcp-NDASM1of1  192  rcp-NDIMP0addall  207  rcp-NDNEGI1  218  rcp-NDNEGE0  223  rcp-NDIME0  228  rcp-NDANDI0  229  rcp-NDANDEL0  230  rcp-NDANDER0  231  rcp-NDORIL0  232  rcp-NDORIR0  233  rcp-NDORE1  234  rcp-NDBII0  239  rcp-NDBIEF0  240  rcp-NDBIER0  241  axL2-P3.22.RC  255  mae-P3.23.RC  258  syl-P3.24.RC  260  dsyl-P3.25.RC  262  rae-P3.26.RC  264  imcomm-P3.27.RC  266  imsubl-P3.28a.RC  268  imsubr-P3.28b.RC  270  imsubd-P3.28c.RC  272  dnegi-P3.29.RC  274  dnege-P3.30.RC  277  trnsp-P3.31a.RC  280  trnsp-P3.31b.RC  283  trnsp-P3.31c.RC  286  trnsp-P3.31d.RC  289  mt-P3.32a.RC  292  nmt-P3.32b.RC  295  bisym-P3.33b.RC  299  bitrns-P3.33c.RC  303  import-P3.34a.RC  306  export-P3.34b.RC  308  subneg-P3.39.RC  324  subiml-P3.40a.RC  326  subimr-P3.40b.RC  328  subimd-P3.40c.RC  330  subbil-P3.41a.RC  333  subbir-P3.41b.RC  335  subbid-P3.41c.RC  337  subandl-P3.42a.RC  340  subandr-P3.42b.RC  342  subandd-P3.42c.RC  344  suborl-P3.43a.RC  347  suborr-P3.43b.RC  349  subord-P3.43c.RC  351  true-P3.44  352  norel-P4.2a.RC  368  norer-P4.2b.RC  371  nandil-P4.3a.RC  374  nandir-P4.3b.RC  376  impoe-P4.4a.RC  378  nimpoe-P4.4b.RC  381  falseimpoe-P4.4c.RC  384  profeliml-P4.5a.RC  386  profelimr-P4.5b.RC  388  nprofeliml-P4.6a.RC  390  nprofelimr-P4.6b.RC  392  falseprofeliml-P4.7a.RC  394  falseprofelimr-P4.7b.RC  396  joinimandinc-P4.8a.RC  398  joinimandres-P4.8b.RC  401  joinimor-P4.8c.RC  404  sepimandr-P4.9a.RC  407  sepimorl-P4.9b.RC  410  sepimorr-P4.9c.RC  413  sepimandl-P4.9d.RC  416  negbicancel-P4.11.RC  420  dnegeint-P4.12.RC  422  negbicancelint-P4.14.RC  425  tsyl-P4.15.RC  427  dbitrns-P4.16.RC  429  tbitrns-P4.17.RC  431  trueie-P4.22a  444  bimpf-P4.RC  532  bimpr-P4.RC  534  subneg2-P4.RC  539  subiml2-P4.RC  541  subimr2-P4.RC  543  subimd2-P4.RC  545  subbil2-P4.RC  547  subbir2-P4.RC  549  subbid2-P4.RC  551  subandl2-P4.RC  553  subandr2-P4.RC  555  subandd2-P4.RC  557  suborl2-P4.RC  559  suborr2-P4.RC  561  subord2-P4.RC  563  andcomm2-P4.RC  565  orcomm2-P4.RC  567  andassoc2a-P4.RC  569  andassoc2b-P4.RC  571  orassoc2a-P4.RC  573  orassoc2b-P4.RC  575  joinimandinc2-P4.RC  577  joinimandinc3-P4.RC  579  joinimandres2-P4.RC  581  joinimandres3-P4.RC  583  joinimor2-P4.RC  585  joinimor3-P4.RC  587  alloverim-P5.RC  589  dalloverim-P5.RC  591  alloverimex-P5.RC  602  dalloverimex-P5.RC  606  ndnfrneg-P7.2.RC  875  ndnfrim-P7.3.RC  876  ndnfrand-P7.4.RC  877  ndnfror-P7.5.RC  878  ndnfrbi-P7.6.RC  879  ndnfrall2-P7.9.RC  880  ndnfrex2-P7.10.RC  881  ndnfrleq-P7.11.RC  882  ndalli-P7.17.RC  883  ndalle-P7.18.RC  885  ndexi-P7.19.RC  886  ndexew-P7.RC  887  ndsubeql-P7.22a.RC  891  ndsubeqr-P7.22b.RC  892  ndsubeqd-P7.RC  893  ndsubelofl-P7.23a.RC  894  ndsubelofr-P7.23b.RC  895  ndsubelofd-P7.RC  896  ndsubsucc-P7.24a.RC  897  ndsubaddl-P7.24b.RC  898  ndsubaddr-P7.24c.RC  899  ndsubaddd-P7.RC  900  ndsubmultl-P7.24d.RC  901  ndsubmultr-P7.24e.RC  902  ndsubmultd-P7.RC  903  nfrgen-P7.RC  929  alloverimex-P7.GENF.RC  950  exia-P7.RC  954  alloverim-P7.GENF.RC  972  suball-P7.RC  974  eqsym-P7r.RC  984  eqtrns-P7.RC  988  alle-P7r.RC  993  exi-P7r.RC  996  exe-P7r.RC  1002  alleexi-P7.RC  1005  alloverim-P7r.RC  1018  dalloverim-P7.RC  1023  dalloverim-P7.GENF.RC  1027  alloverimex-P7r.RC  1029  dalloverimex-P7.RC  1034  dalloverimex-P7.GENF.RC  1038  subex-P7.RC  1044  nfrexgen-P8.RC  1082  nfrexall-P8.RC  1088  nfrnegconv-P8.RC  1111