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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpbiran2d  446  posng  4849  elrnmpt1  5035  fliftf  6008  elxp7  6408  eroveu  6904  sbthlemi5  7283  sbthlemi6  7284  elfi2  7311  sspw1or2  7550  reapltxor  8925  divap0b  9021  nnle1eq1  9337  nn0le0eq0  9602  nn0lt10b  9737  ioopos  10369  xrmaxiflemcom  12040  fz1f1o  12166  nndivdvds  12588  dvdsmultr2  12625  bitsmod  12748  pcmpt  13151  pcmpt2  13152  resrhm2b  14666  lssle0  14818  discld  15362  cncnpi  15454  cnptoprest2  15466  lmss  15472  txcn  15501  isxmet2d  15574  xblss2  15631  bdxmet  15727  xmetxp  15733  cncfcdm  15808  lgsneg  16348  lgsdilem  16351  2lgslem1a  16412  clwwlknonel  16878  clwwlknun  16887  eupth2lem2dc  16905