Theorem anidms 434

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 473  sylancbr 474  anabss1 499  anabss3 500  anabss5 502  so 2859  resiexg 3388  xp11a 3469  xp11b 3470  oe0 4151  oesuc 4156  oecl 4162  nnmsucr 4230  erref 4265  ecopoprdm 4299  php 4499  supsn 4571  r1pwcl 4667  cdainf 4917  recmulpq 5050  ltapq 5056  halfpq 5062  ltsopr 5116  1idsr 5187  00sr 5188  sqgt0sr 5195  ssgt0sr 5197  subidt 5375  leidt 5512  xrltnrt 5522  xrleidt 5541  msqgt0 5595  recextlem1 5663  recextlem2 5664  recext 5665  lt2msqt 5842  le2msqt 5859  2halvest 5994  msqznn 6151  uzindOLD 6164  expubndt 6547  sqnegt 6549  sqclt 6550  subsq2t 6582  bernneq 6591  nnesq 6600  sqr0 6610  sqrlem4 6614  sqrlem5 6615  sqrlem6 6616  sqrlem12 6622  sqrlem21 6631  sqrlem22 6632  sqrlem24 6634  sqrgt0i 6635  sqrlem26 6636  sqr11 6641  sqrmsq2 6644  abssubne0t 6828  faclbnd 6890  faclbnd3 6892  bccl2t 6917  fsum1slem 6954  fsum1ps 6964  2climnn 7047  2climnn0 7048  sin2tt 7412  cos2tt 7413  infxpidmlem7 7509  infxpidmlem10 7512  infxpidmlem12 7514  infdif 7519  idcn 7716  metreslem 7774  cncfmet 7857  isgrp2i 8026  resgrprn 8045  resgrprnOLD 8046  ring2 8101  vcoprnelem 8149  vcoprne 8150  sspmlem 8338  hmoval 8414  pslem 8590  hvsubidt 8834  hvnegidt 8835  hv2timest 8867  hiidrclt 8900  normvalt 8929  chjidmt 9381  normcant 9439  ho2timest 9685  kbpjt 9819  lnop0t 9829  riesz3 9933  leoprft 9999  leopsqt 10000  cvnreft 10156  hmphre 10453  hmeogrp 10461  fipfil2 10475  mslb1 10509

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