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  4736  elrnmpt1  4918  fliftf  5849  elxp7  6237  eroveu  6694  sbthlemi5  7036  sbthlemi6  7037  elfi2  7047  reapltxor  8635  divap0b  8729  nnle1eq1  9033  nn0le0eq0  9296  nn0lt10b  9425  ioopos  10044  xrmaxiflemcom  11433  fz1f1o  11559  nndivdvds  11980  dvdsmultr2  12017  bitsmod  12140  pcmpt  12539  pcmpt2  12540  resrhm2b  13883  lssle0  14006  discld  14480  cncnpi  14572  cnptoprest2  14584  lmss  14590  txcn  14619  isxmet2d  14692  xblss2  14749  bdxmet  14845  xmetxp  14851  cncfcdm  14926  lgsneg  15373  lgsdilem  15376  2lgslem1a  15437