Theorem biantrud 302

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 298	. 2 |- ( ps -> ( ch <-> ( ch /\ ps ) ) )
3	1, 2	syl 14	1 |- ( ph -> ( ch <-> ( ch /\ ps ) ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbiran2d  440  posng  4683  elrnmpt1  4862  fliftf  5778  elxp7  6149  eroveu  6604  sbthlemi5  6938  sbthlemi6  6939  elfi2  6949  reapltxor  8508  divap0b  8600  nnle1eq1  8902  nn0le0eq0  9163  nn0lt10b  9292  ioopos  9907  xrmaxiflemcom  11212  fz1f1o  11338  nndivdvds  11758  dvdsmultr2  11795  pcmpt  12295  pcmpt2  12296  discld  12930  cncnpi  13022  cnptoprest2  13034  lmss  13040  txcn  13069  isxmet2d  13142  xblss2  13199  bdxmet  13295  xmetxp  13301  cncffvrn  13363  lgsneg  13719  lgsdilem  13722