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  439  posng  4676  elrnmpt1  4855  fliftf  5767  elxp7  6138  eroveu  6592  sbthlemi5  6926  sbthlemi6  6927  elfi2  6937  reapltxor  8487  divap0b  8579  nnle1eq1  8881  nn0le0eq0  9142  nn0lt10b  9271  ioopos  9886  xrmaxiflemcom  11190  fz1f1o  11316  nndivdvds  11736  dvdsmultr2  11773  pcmpt  12273  pcmpt2  12274  discld  12776  cncnpi  12868  cnptoprest2  12880  lmss  12886  txcn  12915  isxmet2d  12988  xblss2  13045  bdxmet  13141  xmetxp  13147  cncffvrn  13209  lgsneg  13565  lgsdilem  13568