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  4746  elrnmpt1  4928  fliftf  5867  elxp7  6255  eroveu  6712  sbthlemi5  7062  sbthlemi6  7063  elfi2  7073  reapltxor  8661  divap0b  8755  nnle1eq1  9059  nn0le0eq0  9322  nn0lt10b  9452  ioopos  10071  xrmaxiflemcom  11531  fz1f1o  11657  nndivdvds  12078  dvdsmultr2  12115  bitsmod  12238  pcmpt  12637  pcmpt2  12638  resrhm2b  13982  lssle0  14105  discld  14579  cncnpi  14671  cnptoprest2  14683  lmss  14689  txcn  14718  isxmet2d  14791  xblss2  14848  bdxmet  14944  xmetxp  14950  cncfcdm  15025  lgsneg  15472  lgsdilem  15475  2lgslem1a  15536