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  7545  reapltxor  8920  divap0b  9016  nnle1eq1  9331  nn0le0eq0  9596  nn0lt10b  9731  ioopos  10363  xrmaxiflemcom  12034  fz1f1o  12160  nndivdvds  12582  dvdsmultr2  12619  bitsmod  12742  pcmpt  13145  pcmpt2  13146  resrhm2b  14641  lssle0  14793  discld  15328  cncnpi  15420  cnptoprest2  15432  lmss  15438  txcn  15467  isxmet2d  15540  xblss2  15597  bdxmet  15693  xmetxp  15699  cncfcdm  15774  lgsneg  16309  lgsdilem  16312  2lgslem1a  16373  clwwlknonel  16839  clwwlknun  16848  eupth2lem2dc  16866