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  3933  pwnss  4219  posng  4765  sqxpexg  4809  xpid11  4920  resiexg  5023  f1mpt  5863  f1eqcocnv  5883  isopolem  5914  poxp  6341  nnmsucr  6597  erex  6667  ecopover  6743  ecopoverg  6746  enrefg  6878  3xpfi  7056  tapeq2  7400  netap  7401  2omotaplemap  7404  ltsopi  7468  recexnq  7538  ltsonq  7546  ltaddnq  7555  nsmallnqq  7560  ltpopr  7743  ltposr  7911  1idsr  7916  00sr  7917  axltirr  8174  leid  8191  reapirr  8685  inelr  8692  apsqgt0  8709  apirr  8713  msqge0  8724  recextlem1  8759  recexaplem2  8760  recexap  8761  div1  8811  cju  9069  2halves  9301  msqznn  9508  xrltnr  9936  xrleid  9957  iooidg  10066  iccid  10082  m1expeven  10768  expubnd  10778  sqneg  10780  sqcl  10782  sqap0  10788  nnsqcl  10791  qsqcl  10793  subsq2  10829  bernneq  10842  faclbnd  10923  faclbnd3  10925  cjmulval  11314  sin2t  12175  cos2t  12176  gcd0id  12415  lcmid  12517  lcmgcdeq  12520  intopsn  13314  mgm1  13317  sgrp1  13358  mnd1  13402  mnd1id  13403  grpsubid  13531  grp1  13553  grp1inv  13554  ringadd2  13904  ring1  13936  idcn  14799  ismet  14931  isxmet  14932  resubmet  15143  bj-snexg  16047