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  4822  elrnmpt1  5008  fliftf  5972  elxp7  6364  eroveu  6860  sbthlemi5  7231  sbthlemi6  7232  elfi2  7259  sspw1or2  7495  reapltxor  8863  divap0b  8957  nnle1eq1  9261  nn0le0eq0  9524  nn0lt10b  9658  ioopos  10283  xrmaxiflemcom  11934  fz1f1o  12060  nndivdvds  12482  dvdsmultr2  12519  bitsmod  12642  pcmpt  13041  pcmpt2  13042  resrhm2b  14394  lssle0  14520  discld  15001  cncnpi  15093  cnptoprest2  15105  lmss  15111  txcn  15140  isxmet2d  15213  xblss2  15270  bdxmet  15366  xmetxp  15372  cncfcdm  15447  lgsneg  15897  lgsdilem  15900  2lgslem1a  15961  clwwlknonel  16427  clwwlknun  16436  eupth2lem2dc  16454