Theorem anidms 436

Description: Inference from idempotent law for conjunction.

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  sylancb 475  sylancbr 476  anabss1 501  anabss3 502  anabss5 504  so 2870  resiexg 3402  xp11a 3483  xp11b 3484  oe0 4167  oesuc 4172  oecl 4178  nnmsucr 4246  erref 4281  ecopoprdm 4315  php 4519  supsn 4600  r1pwcl 4697  cdainf 4949  recmulpq 5082  ltapq 5088  halfpq 5094  ltsopr 5148  1idsr 5219  00sr 5220  sqgt0sr 5227  ssgt0sr 5229  subidt 5407  leidt 5543  xrltnrt 5553  xrleidt 5572  msqgt0 5625  recextlem1 5694  recextlem2 5695  recext 5696  lt2msqt 5888  le2msqt 5905  2halvest 6041  msqznn 6198  uzindOLD 6210  expubndt 6609  sqnegt 6611  sqclt 6612  subsq2t 6644  bernneq 6653  nnesq 6663  sqr0 6673  sqrlem4 6677  sqrlem5 6678  sqrlem6 6679  sqrlem12 6685  sqrlem21 6694  sqrlem22 6695  sqrlem24 6697  sqrgt0i 6698  sqrlem26 6699  sqr11 6704  sqrmsq2 6707  abssubne0t 6882  faclbnd 6945  faclbnd3 6947  bccl2t 6971  fsum1slem 7008  fsum1ps 7018  2climnn 7102  2climnn0 7103  sin2tt 7462  cos2tt 7463  infxpidmlem7 7559  infxpidmlem10 7562  infxpidmlem12 7564  infdif 7569  idcn 7763  metreslem 7819  cncfmet 7902  isgrp2i 8072  resgrprn 8091  ring2 8145  vcoprnelem 8193  vcoprne 8194  sspmlem 8387  hmoval 8466  pslem 8643  hvsubidt 8890  hvnegidt 8891  hv2timest 8923  hiidrclt 8956  normvalt 8985  chjidmt 9438  normcant 9494  ho2timest 9740  kbpjt 9875  lnop0t 9885  riesz3 9990  leoprft 10056  leopsqt 10057  cvnreft 10213  inposet 10477  hmphre 10516  hmeogrp 10524  fipfil2 10550  mslb1 10600

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain