Theorem biantrud 304

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.)

Hypothesis

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

Assertion

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

Proof of Theorem biantrud

Step	Hyp	Ref	Expression
1		biantrud.1	. 2 |- ( ph -> ps )
2		iba 300	. 2 |- ( ps -> ( ch <-> ( ch /\ ps ) ) )
3	1, 2	syl 14	1 |- ( ph -> ( ch <-> ( ch /\ ps ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbiran2d  442  posng  4798  elrnmpt1  4983  fliftf  5940  elxp7  6333  eroveu  6795  sbthlemi5  7160  sbthlemi6  7161  elfi2  7171  sspw1or2  7403  reapltxor  8769  divap0b  8863  nnle1eq1  9167  nn0le0eq0  9430  nn0lt10b  9560  ioopos  10185  xrmaxiflemcom  11827  fz1f1o  11953  nndivdvds  12375  dvdsmultr2  12412  bitsmod  12535  pcmpt  12934  pcmpt2  12935  resrhm2b  14282  lssle0  14405  discld  14879  cncnpi  14971  cnptoprest2  14983  lmss  14989  txcn  15018  isxmet2d  15091  xblss2  15148  bdxmet  15244  xmetxp  15250  cncfcdm  15325  lgsneg  15772  lgsdilem  15775  2lgslem1a  15836  clwwlknonel  16302  clwwlknun  16311  eupth2lem2dc  16329