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  4791  elrnmpt1  4975  fliftf  5923  elxp7  6316  eroveu  6773  sbthlemi5  7128  sbthlemi6  7129  elfi2  7139  reapltxor  8736  divap0b  8830  nnle1eq1  9134  nn0le0eq0  9397  nn0lt10b  9527  ioopos  10146  xrmaxiflemcom  11760  fz1f1o  11886  nndivdvds  12307  dvdsmultr2  12344  bitsmod  12467  pcmpt  12866  pcmpt2  12867  resrhm2b  14213  lssle0  14336  discld  14810  cncnpi  14902  cnptoprest2  14914  lmss  14920  txcn  14949  isxmet2d  15022  xblss2  15079  bdxmet  15175  xmetxp  15181  cncfcdm  15256  lgsneg  15703  lgsdilem  15706  2lgslem1a  15767