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  4790  elrnmpt1  4974  fliftf  5922  elxp7  6314  eroveu  6771  sbthlemi5  7124  sbthlemi6  7125  elfi2  7135  reapltxor  8732  divap0b  8826  nnle1eq1  9130  nn0le0eq0  9393  nn0lt10b  9523  ioopos  10142  xrmaxiflemcom  11755  fz1f1o  11881  nndivdvds  12302  dvdsmultr2  12339  bitsmod  12462  pcmpt  12861  pcmpt2  12862  resrhm2b  14207  lssle0  14330  discld  14804  cncnpi  14896  cnptoprest2  14908  lmss  14914  txcn  14943  isxmet2d  15016  xblss2  15073  bdxmet  15169  xmetxp  15175  cncfcdm  15250  lgsneg  15697  lgsdilem  15700  2lgslem1a  15761