Theorem biantrurd 796

Description: A wff is equivalent to its conjunction with truth. (The proof was shortened by Andrew Salmon, 7-May-2011.)

Hypothesis

Ref	Expression
biantrud.1	|- (ph -> ps)

Assertion

Ref	Expression
biantrurd	|- (ph -> (ch <-> (ps /\ ch)))

Proof of Theorem biantrurd

Step	Hyp	Ref	Expression
1		biantrud.1	. 2 |- (ph -> ps)
2		ibar 705	. 2 |- (ps -> (ch <-> (ps /\ ch)))
3	1, 2	syl 12	1 |- (ph -> (ch <-> (ps /\ ch)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  sbcgfOLD 2521  n0moeu 2887  reldisjOLD 2917  euexeqOLD 3826  euexaleq 3827  reuxfrd 3846  opbrop 4064  funcnv3 4476  fnssresb 4525  dffo3 4792  fconst4 4827  eloprabg 4936  mapxpen 5589  bnd2 5854  kmlem2 5928  iscard2 6006  supxrre 7292  supxrre1 7302  elnnnn0 7381  znnsub 7386  znn0sub 7387  icounlem 7581  elfz5 7644  cau3ii 8166  dffsum 8258  qdensere 9027  metgt0 9097  lmbrf 9208  lmbrf2 9209  iscauf 9217  iscau5 9219  iscaunns 9222  lmclimnn 9242  nmo0 9791  pilem1 10020  pilem3 10022  axgroth2 10133  isflimf 10323  h2hcau 10481  h2hlm 10482  ch0pss 11002  pjnorm2 11307  dfbdop2 11423  leop 11694  atcv0eq 11951  bnj1457 13138  elo 14342  eltids 14369  dffprod 14670  conttnf 14944  heiborlem23 15977  rrnmet 16016  isdmn3 16222  latleeqm1 16874  latnlemlt 16879  latnle 16880  op1le 16919  leatom 17005  hlrelat5 17050  hlrelat 17051  cvrexchlem 17059  atcvr0eq 17064  elpadd2at2 17268

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