Theorem rcp-NDASM2of2 194

Description: ( 1 ∧ 2 ) → 2. †

Assertion

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

Proof of Theorem rcp-NDASM2of2

Step	Hyp	Ref	Expression
1		ndasm-P3.1 166	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

This theorem is referenced by:  rcp-NDASM2of3  196  rcp-NDNEGI1  218  rcp-NDORE1  234  ndnege-P3.4.CL  243  ndime-P3.6.CL  244  ndbii-P3.13.CL  248  mae-P3.23  257  syl-P3.24  259  rae-P3.26  263  imsubl-P3.28a  267  imsubr-P3.28b  269  dnegi-P3.29  273  dnege-P3.30  276  mt-P3.32a  291  nmt-P3.32b  294  bitrns-P3.33c.CL  304  import-P3.34a  305  example-E3.2b  312  orcomm-P3.37-L1  318  orassoc-P3.38-L1  320  orassoc-P3.38-L2  321  subbil-P3.41a-L1  331  subandl-P3.42a-L1  338  suborl-P3.43a-L1  345  andasim-P3.46-L1  354  andasim-P3.46-L2  355  orasim-P3.48-L2  360  ncontra-P4.1  366  norel-P4.2a  367  norer-P4.2b  370  nandil-P4.3a  373  nandir-P4.3b  375  impoe-P4.4a  377  nimpoe-P4.4b  380  profeliml-P4.5a  385  profelimr-P4.5b  387  nprofeliml-P4.6a  389  nprofelimr-P4.6b  391  falseprofeliml-P4.7a  393  falseprofelimr-P4.7b  395  joinimandinc-P4.8a  397  joinimandres-P4.8b  400  sepimandr-P4.9a  406  sepimorl-P4.9b  409  sepimorr-P4.9c  412  sepimandl-P4.9d  415  dnegeint-P4.12  421  idandtruel-P4.19a  438  idorfalsel-P4.20a  440  falseie-P4.22b  445  idempotor-P4.25b  451  dmorgarev-L4.2  453  dmorgbrev-L4.4  455  andoveror-P4.27-L1  459  andoveror-P4.27-L2  460  oroverand-P4.27-L3  462  oroverim-P4.28-L2  466  imoverim-P4.30-L1  476  imasor-P4.32-L1  485  imasor-P4.32-L2  486  imasandint-P4.33b  490  biasandorint-P4.34b  492  peirce-P4.40  511  exclmid2peirce-P4.41a  512  impime-P4  526  eqtrns-P5.CL  631  subelofd-P5.CL  643  subaddd-P5.CL  648  submultd-P5.CL  652  eqmiddle-P6  708  spliteq-P6-L1  775  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  axL4ex-P7  946  allnegex-P7-L1  956  eqtrns-P7.CL  989  exnegallint-P7  1047  qimeqex-P7-L1  1054