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  4827  elrnmpt1  5013  fliftf  5978  elxp7  6377  eroveu  6873  sbthlemi5  7244  sbthlemi6  7245  elfi2  7272  sspw1or2  7508  reapltxor  8880  divap0b  8974  nnle1eq1  9278  nn0le0eq0  9541  nn0lt10b  9676  ioopos  10302  xrmaxiflemcom  11959  fz1f1o  12085  nndivdvds  12507  dvdsmultr2  12544  bitsmod  12667  pcmpt  13066  pcmpt2  13067  resrhm2b  14495  lssle0  14646  discld  15127  cncnpi  15219  cnptoprest2  15231  lmss  15237  txcn  15266  isxmet2d  15339  xblss2  15396  bdxmet  15492  xmetxp  15498  cncfcdm  15573  lgsneg  16023  lgsdilem  16026  2lgslem1a  16087  clwwlknonel  16553  clwwlknun  16562  eupth2lem2dc  16580