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  4847  elrnmpt1  5033  fliftf  6005  elxp7  6404  eroveu  6900  sbthlemi5  7278  sbthlemi6  7279  elfi2  7306  sspw1or2  7544  reapltxor  8917  divap0b  9013  nnle1eq1  9328  nn0le0eq0  9591  nn0lt10b  9726  ioopos  10352  xrmaxiflemcom  12015  fz1f1o  12141  nndivdvds  12563  dvdsmultr2  12600  bitsmod  12723  pcmpt  13122  pcmpt2  13123  resrhm2b  14557  lssle0  14709  discld  15237  cncnpi  15329  cnptoprest2  15341  lmss  15347  txcn  15376  isxmet2d  15449  xblss2  15506  bdxmet  15602  xmetxp  15608  cncfcdm  15683  lgsneg  16143  lgsdilem  16146  2lgslem1a  16207  clwwlknonel  16673  clwwlknun  16682  eupth2lem2dc  16700