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  4798  elrnmpt1  4983  fliftf  5939  elxp7  6332  eroveu  6794  sbthlemi5  7159  sbthlemi6  7160  elfi2  7170  sspw1or2  7402  reapltxor  8768  divap0b  8862  nnle1eq1  9166  nn0le0eq0  9429  nn0lt10b  9559  ioopos  10184  xrmaxiflemcom  11809  fz1f1o  11935  nndivdvds  12356  dvdsmultr2  12393  bitsmod  12516  pcmpt  12915  pcmpt2  12916  resrhm2b  14262  lssle0  14385  discld  14859  cncnpi  14951  cnptoprest2  14963  lmss  14969  txcn  14998  isxmet2d  15071  xblss2  15128  bdxmet  15224  xmetxp  15230  cncfcdm  15305  lgsneg  15752  lgsdilem  15755  2lgslem1a  15816  clwwlknonel  16282  clwwlknun  16291  eupth2lem2dc  16309