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  8919  divap0b  9015  nnle1eq1  9330  nn0le0eq0  9595  nn0lt10b  9730  ioopos  10362  xrmaxiflemcom  12031  fz1f1o  12157  nndivdvds  12579  dvdsmultr2  12616  bitsmod  12739  pcmpt  13142  pcmpt2  13143  resrhm2b  14606  lssle0  14758  discld  15286  cncnpi  15378  cnptoprest2  15390  lmss  15396  txcn  15425  isxmet2d  15498  xblss2  15555  bdxmet  15651  xmetxp  15657  cncfcdm  15732  lgsneg  16241  lgsdilem  16244  2lgslem1a  16305  clwwlknonel  16771  clwwlknun  16780  eupth2lem2dc  16798