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  4760  elrnmpt1  4943  fliftf  5886  elxp7  6274  eroveu  6731  sbthlemi5  7084  sbthlemi6  7085  elfi2  7095  reapltxor  8692  divap0b  8786  nnle1eq1  9090  nn0le0eq0  9353  nn0lt10b  9483  ioopos  10102  xrmaxiflemcom  11645  fz1f1o  11771  nndivdvds  12192  dvdsmultr2  12229  bitsmod  12352  pcmpt  12751  pcmpt2  12752  resrhm2b  14096  lssle0  14219  discld  14693  cncnpi  14785  cnptoprest2  14797  lmss  14803  txcn  14832  isxmet2d  14905  xblss2  14962  bdxmet  15058  xmetxp  15064  cncfcdm  15139  lgsneg  15586  lgsdilem  15589  2lgslem1a  15650