Theorem rcp-NDASM1of2 193

Description: ( 1 ∧ 2 ) → 1. †

Assertion

Ref	Expression
rcp-NDASM1of2	⊢ ((𝛾₁ ∧ 𝛾₂) → 𝛾₁)

Proof of Theorem rcp-NDASM1of2

Step	Hyp	Ref	Expression
1		rcp-NDASM1of1 192	. 2 ⊢ (𝛾₁ → 𝛾₁)
2	1	ndimp-P3.2 167	1 ⊢ ((𝛾₁ ∧ 𝛾₂) → 𝛾₁)

Syntax hints:   → wff-imp 10   ∧ wff-and 132

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-NDASM1of3  195  ndnege-P3.4.CL  243  ndime-P3.6.CL  244  ndbii-P3.13.CL  248  bitrns-P3.33c.CL  304  andasim-P3.46-L1  354  andasim-P3.46-L2  355  orasim-P3.48-L1  359  orasim-P3.48-L2  360  ncontra-P4.1  366  falseie-P4.22b  445  idempotand-P4.25a  450  oroverand-P4.27-L4  463  imoverim-P4.30-L1  476  imasor-P4.32-L1  485  imasandint-P4.33b  490  peirce-P4.40  511  exclmid2peirce-P4.41a  512  eqtrns-P5.CL  631  subelofd-P5.CL  643  subaddd-P5.CL  648  submultd-P5.CL  652  lemma-L6.07a-L2  771  spliteq-P6-L1  775  splitelof-P6-L1  777  psubsuccv-P6-L1  805  ndnfrim-P7.3.CL  905  ndnfrand-P7.4.CL  906  ndnfror-P7.5.CL  907  ndnfrbi-P7.6.CL  908  ndsubeqd-P7.CL  913  ndsubelofd-P7.CL  916  ndsubaddd-P7.CL  920  ndsubmultd-P7.CL  923  eqtrns-P7.CL  989  exnegallint-P7  1047  qimeqex-P7-L2  1055