Theorem anidms 397

Description: Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)

Hypothesis

Ref	Expression
anidms.1	|- ( ( ph /\ ph ) -> ps )

Assertion

Ref	Expression
anidms	|- ( ph -> ps )

Proof of Theorem anidms

Step	Hyp	Ref	Expression
1		anidms.1	. . 3 |- ( ( ph /\ ph ) -> ps )
2	1	ex 115	. 2 |- ( ph -> ( ph -> ps ) )
3	2	pm2.43i 49	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  sylancb  418  sylancbr  419  intsng  3919  pwnss  4204  posng  4748  sqxpexg  4792  xpid11  4902  resiexg  5005  f1mpt  5842  f1eqcocnv  5862  isopolem  5893  poxp  6320  nnmsucr  6576  erex  6646  ecopover  6722  ecopoverg  6725  enrefg  6857  3xpfi  7032  tapeq2  7367  netap  7368  2omotaplemap  7371  ltsopi  7435  recexnq  7505  ltsonq  7513  ltaddnq  7522  nsmallnqq  7527  ltpopr  7710  ltposr  7878  1idsr  7883  00sr  7884  axltirr  8141  leid  8158  reapirr  8652  inelr  8659  apsqgt0  8676  apirr  8680  msqge0  8691  recextlem1  8726  recexaplem2  8727  recexap  8728  div1  8778  cju  9036  2halves  9268  msqznn  9475  xrltnr  9903  xrleid  9924  iooidg  10033  iccid  10049  m1expeven  10733  expubnd  10743  sqneg  10745  sqcl  10747  sqap0  10753  nnsqcl  10756  qsqcl  10758  subsq2  10794  bernneq  10807  faclbnd  10888  faclbnd3  10890  cjmulval  11232  sin2t  12093  cos2t  12094  gcd0id  12333  lcmid  12435  lcmgcdeq  12438  intopsn  13232  mgm1  13235  sgrp1  13276  mnd1  13320  mnd1id  13321  grpsubid  13449  grp1  13471  grp1inv  13472  ringadd2  13822  ring1  13854  idcn  14717  ismet  14849  isxmet  14850  resubmet  15061  bj-snexg  15885