Theorem anidms 480

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  sylancb 529  sylancbr 530  anabss1 557  anabss3 558  anabss5 560  dedth2v 3018  dedth3v 3019  so 3620  xpid11 4181  resiexg 4253  xp11bOLD 4349  xp11aOLD 4351  oe0 5206  oesuc 5211  oecl 5218  oeclOLD 5219  nnmsucr 5295  nnmsucrOLD 5296  erref 5333  ecopoprdm 5368  php 5607  supsn 5681  hartog 5693  r1pwcl 5798  cdainf 6087  recmulpq 6222  ltapq 6228  halfpq 6234  ltsopr 6288  1idsr 6359  00sr 6360  sqgt0sr 6367  ssgt0sr 6369  subid 6555  leid 6701  xrltnr 6716  xrleid 6735  msqgt0i 6794  recextlem1 6874  recextlem2 6875  recex 6876  lt2msq 7069  le2msq 7086  2halves 7225  msqznn 7408  uzindOLD 7420  expubnd 7853  sqneg 7855  sqcl 7856  subsq2 7889  bernneq 7898  bernneqOLD 7899  nnesqi 7912  sqr0 7922  sqrlem4 7926  sqrlem5 7927  sqrlem6 7928  sqrlem12 7934  sqrlem21 7943  sqrlem22 7944  sqrlem24 7946  sqrgt0ii 7947  sqrlem26 7948  sqr11i 7953  sqrmsq2i 7956  abssubne0 8134  faclbnd 8197  faclbnd3 8199  bccl2 8223  fsum1slem 8268  fsum1ps 8278  2climnn 8362  2climnn0 8363  sin2t 8727  cos2t 8728  infxpidmlem7 8827  infxpidmlem10 8830  infxpidmlem12 8832  infdif 8837  idcn 9042  metreslem 9099  cncfmet 9183  isgrp2i 9360  resgrprn 9403  ring2 9474  vcoprnelem 9529  vcoprne 9530  hmoval 9810  pslem 9990  basmetres 10185  fipfil2 10272  dirref 10355  ismgm 10367  opidon2 10371  on1el3 10412  on1el4 10413  hvsubid 10527  hvnegid 10528  hv2times 10560  hiidrcl 10594  normval 10623  chjidm 11076  normcan 11132  ho2times 11382  kbpj 11517  lnop0 11527  riesz3i 11632  leoprf 11699  leopsq 11700  opsqrlem3 11713  cvnref 11863  fseq1cl 13619  divalglem0 13696  divalglem2 13698  gcd0id 13729  predpoirr 13908  predfrirr 13909  poxp 13949  elfix2 14078  nabi2 14140  cnvref 14371  islatalg 14531  jidd 14540  midd 14541  preoref22 14570  sqpre 14579  inposet 14620  fprod1slem 14676  ridlideq 14695  rzrlzreq 14696  svs2 14829  hmphre 14884  hmeogrp 14892  topgrpi 14972  trhom 14983  mslb1 15007  dualalg 15131  catsbc 15197  tarsuc2 15245  ccid 15363  hartogOLD 15384  enf1f1o 15720  metf1o 15843  stioo 15845  iccst 15875  txmet 15925  heiborlem16 15970  heiborlem36 15990  exidreslem 16030  pcohtpylem3 16082  pcopt 16084  pi1f 16093

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 164  df-an 242

Copyright terms: Public domain