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  4732  elrnmpt1  4914  fliftf  5843  elxp7  6225  eroveu  6682  sbthlemi5  7022  sbthlemi6  7023  elfi2  7033  reapltxor  8610  divap0b  8704  nnle1eq1  9008  nn0le0eq0  9271  nn0lt10b  9400  ioopos  10019  xrmaxiflemcom  11395  fz1f1o  11521  nndivdvds  11942  dvdsmultr2  11979  pcmpt  12484  pcmpt2  12485  resrhm2b  13748  lssle0  13871  discld  14315  cncnpi  14407  cnptoprest2  14419  lmss  14425  txcn  14454  isxmet2d  14527  xblss2  14584  bdxmet  14680  xmetxp  14686  cncfcdm  14761  lgsneg  15181  lgsdilem  15184  2lgslem1a  15245