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  438  posng  4611  elrnmpt1  4790  fliftf  5700  elxp7  6068  eroveu  6520  sbthlemi5  6849  sbthlemi6  6850  elfi2  6860  reapltxor  8351  divap0b  8443  nnle1eq1  8744  nn0le0eq0  9005  nn0lt10b  9131  ioopos  9733  xrmaxiflemcom  11018  fz1f1o  11144  nndivdvds  11499  dvdsmultr2  11533  discld  12305  cncnpi  12397  cnptoprest2  12409  lmss  12415  txcn  12444  isxmet2d  12517  xblss2  12574  bdxmet  12670  xmetxp  12676  cncffvrn  12738