Theorem anidms 389

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  sylancb  409  sylancbr  410  intsng  3670  pwnss  3933  posng  4430  xpid11m  4575  resiexg  4673  f1mpt  5431  f1eqcocnv  5451  isopolem  5481  poxp  5873  nnmsucr  6090  erex  6153  ecopover  6227  ecopoverg  6230  enrefg  6267  ltsopi  6510  recexnq  6580  ltsonq  6588  ltaddnq  6597  nsmallnqq  6602  ltpopr  6785  ltposr  6940  1idsr  6945  00sr  6946  axltirr  7179  leid  7195  reapirr  7677  inelr  7684  apsqgt0  7701  apirr  7705  msqge0  7716  recextlem1  7741  recexaplem2  7742  recexap  7743  div1  7791  cju  8038  2halves  8260  msqznn  8447  xrltnr  8855  xrleid  8874  iooidg  8932  iccid  8948  m1expeven  9523  expubnd  9533  sqneg  9535  sqcl  9537  sqap0  9542  nnsqcl  9545  qsqcl  9547  subsq2  9582  bernneq  9593  faclbnd  9668  faclbnd3  9670  cjmulval  9775  gcd0id  10370  lcmid  10462  lcmgcdeq  10465  bj-snexg  10703