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  11502  fz1f1o  11628  nndivdvds  12049  dvdsmultr2  12086  bitsmod  12209  pcmpt  12608  pcmpt2  12609  resrhm2b  13953  lssle0  14076  discld  14550  cncnpi  14642  cnptoprest2  14654  lmss  14660  txcn  14689  isxmet2d  14762  xblss2  14819  bdxmet  14915  xmetxp  14921  cncfcdm  14996  lgsneg  15443  lgsdilem  15446  2lgslem1a  15507