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  4796  elrnmpt1  4981  fliftf  5935  elxp7  6328  eroveu  6790  sbthlemi5  7151  sbthlemi6  7152  elfi2  7162  reapltxor  8759  divap0b  8853  nnle1eq1  9157  nn0le0eq0  9420  nn0lt10b  9550  ioopos  10175  xrmaxiflemcom  11800  fz1f1o  11926  nndivdvds  12347  dvdsmultr2  12384  bitsmod  12507  pcmpt  12906  pcmpt2  12907  resrhm2b  14253  lssle0  14376  discld  14850  cncnpi  14942  cnptoprest2  14954  lmss  14960  txcn  14989  isxmet2d  15062  xblss2  15119  bdxmet  15215  xmetxp  15221  cncfcdm  15296  lgsneg  15743  lgsdilem  15746  2lgslem1a  15807  clwwlknonel  16227  clwwlknun  16236