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  6905  sbthlemi5  7285  sbthlemi6  7286  elfi2  7311  sspw1or2  7550  reapltxor  8925  divap0b  9021  nnle1eq1  9337  nn0le0eq0  9602  nn0lt10b  9735  ioopos  10368  xrmaxiflemcom  12039  fz1f1o  12165  nndivdvds  12587  dvdsmultr2  12624  bitsmod  12747  pcmpt  13150  pcmpt2  13151  resrhm2b  14665  lssle0  14817  discld  15379  cncnpi  15471  cnptoprest2  15483  lmss  15489  txcn  15518  isxmet2d  15591  xblss2  15648  bdxmet  15744  xmetxp  15750  cncfcdm  15825  lgsneg  16365  lgsdilem  16368  2lgslem1a  16429  clwwlknonel  16895  clwwlknun  16904  eupth2lem2dc  16922