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  4692  elrnmpt1  4871  fliftf  5790  elxp7  6161  eroveu  6616  sbthlemi5  6950  sbthlemi6  6951  elfi2  6961  reapltxor  8520  divap0b  8612  nnle1eq1  8914  nn0le0eq0  9175  nn0lt10b  9304  ioopos  9919  xrmaxiflemcom  11223  fz1f1o  11349  nndivdvds  11769  dvdsmultr2  11806  pcmpt  12306  pcmpt2  12307  discld  13187  cncnpi  13279  cnptoprest2  13291  lmss  13297  txcn  13326  isxmet2d  13399  xblss2  13456  bdxmet  13552  xmetxp  13558  cncfcdm  13620  lgsneg  13976  lgsdilem  13979