Theorem anidms 395

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 114	. 2 |- ( ph -> ( ph -> ps ) )
3	2	pm2.43i 49	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  sylancb  415  sylancbr  416  intsng  3841  pwnss  4119  posng  4655  sqxpexg  4699  xpid11  4806  resiexg  4908  f1mpt  5716  f1eqcocnv  5736  isopolem  5767  poxp  6173  nnmsucr  6428  erex  6497  ecopover  6571  ecopoverg  6574  enrefg  6702  3xpfi  6868  ltsopi  7223  recexnq  7293  ltsonq  7301  ltaddnq  7310  nsmallnqq  7315  ltpopr  7498  ltposr  7666  1idsr  7671  00sr  7672  axltirr  7927  leid  7944  reapirr  8435  inelr  8442  apsqgt0  8459  apirr  8463  msqge0  8474  recextlem1  8508  recexaplem2  8509  recexap  8510  div1  8559  cju  8815  2halves  9045  msqznn  9247  xrltnr  9668  xrleid  9689  iooidg  9795  iccid  9811  m1expeven  10448  expubnd  10458  sqneg  10460  sqcl  10462  sqap0  10467  nnsqcl  10470  qsqcl  10472  subsq2  10508  bernneq  10520  faclbnd  10597  faclbnd3  10599  cjmulval  10770  sin2t  11628  cos2t  11629  gcd0id  11843  lcmid  11937  lcmgcdeq  11940  idcn  12572  ismet  12704  isxmet  12705  resubmet  12908  bj-snexg  13447