Theorem rcp-NDASM1of1 192

Description: ( 1 ) → 1. †

Assertion

Ref	Expression
rcp-NDASM1of1	⊢ (𝛾₁ → 𝛾₁)

Proof of Theorem rcp-NDASM1of1

Step	Hyp	Ref	Expression
1		ndasm-P3.1 166	. . 3 ⊢ ((⊤ ∧ 𝛾₁) → 𝛾₁)
2	1	ndimi-P3.5 170	. 2 ⊢ (⊤ → (𝛾₁ → 𝛾₁))
3	2	ndtruee-P3.18 183	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-and-D2.2 133  df-true-D2.4 155

This theorem is referenced by:  rcp-NDASM1of2  193  ndoril-P3.10.CL  245  ndorir-P3.11.CL  246  ndbief-P3.14.CL  249  ndbier-P3.15.CL  250  axL1-P3.21.CL  253  axL2-P3.22.CL  256  dnegi-P3.29.CL  275  dnege-P3.30.CL  278  trnsp-P3.31a.CL  281  trnsp-P3.31b.CL  284  trnsp-P3.31c.CL  287  trnsp-P3.31d.CL  290  mt-3.32a.CL  293  nmt-3.32b.CL  296  biref-P3.33a  297  bisym-P3.33b.CL  300  andcomm-P3.35-L1  313  andassoc-P3.36-L1  315  andassoc-P3.36-L2  316  orcomm-P3.37-L1  318  orassoc-P3.38-L1  320  orassoc-P3.38-L2  321  true-P3.44  352  false-P3.45  353  norel-P4.2a.CL  369  norer-P4.2b.CL  372  impoe-P4.4a.CL  379  nimpoe-P4.4b.CL  382  joinimandinc-P4.8a.CL  399  joinimandres-P4.8b.CL  402  joinimor-P4.8c.CL  405  sepimandr-P4.9a.CL  408  sepimorl-P4.9b.CL  411  sepimorr-P4.9c.CL  414  sepimandl-P4.9d.CL  417  dnegeqint-P4.13  423  idandtruel-P4.19a  438  idorfalsel-P4.20a  440  nthmeqfalse-P4.21b  443  falseie-P4.22b  445  idempotand-P4.25a  450  idempotor-P4.25b  451  dmorgbrev-L4.4  455  andoveror-P4.27-L2  460  oroverand-P4.27-L3  462  imasor-P4.32-L2  486  biasandorint-P4.34b  492  truthtblfimt-P4.36c  497  truthtblfimf-P4.36d  498  alloverimex-P5.CL  604  qimeqallbv-P5-L1  619  eqsym-P5.CL  628  subeql-P5.CL  633  subeqr-P5.CL  636  subelofl-P5.CL  639  subelofr-P5.CL  641  example-E5.01a  663  example-E5.02a  664  example-E5.03a  665  example-E5.04a  675  eqmiddle-P6.CL  709  ndnfrneg-P7.2.CL  904  ndalle-P7.18.CL  909  ndexi-P7.19.CL  910  ndsubeql-P7.22a.CL  911  ndsubeqr-P7.22b.CL  912  ndsubelofl-P7.23a.CL  914  ndsubelofr-P7.23b.CL  915  ndsubsucc-P7.24a.CL  917  ndsubaddl-P7.24b.CL  918  ndsubaddr-P7.24c.CL  919  ndsubmultl-P7.24d.CL  921  ndsubmultr-P7.24e.CL  922  nfrgen-P7.CL  930  nfrexgen-P7.CL  932  eqsym-P7.CL  937  alle-P7.CL  942  exi-P7.CL  952  nfrgencl-P7  965  alleexi-P7.CL  1006  dalloverim-P7.CL  1024  dalloverimex-P7.CL  1035  qimeqex-P7-L1  1054  nfrexall-P8.CL  1090  nfrnegconv-P8.CL  1112