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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbiran2d  446  posng  4842  elrnmpt1  5028  fliftf  5995  elxp7  6394  eroveu  6890  sbthlemi5  7268  sbthlemi6  7269  elfi2  7296  sspw1or2  7534  reapltxor  8907  divap0b  9003  nnle1eq1  9307  nn0le0eq0  9570  nn0lt10b  9705  ioopos  10331  xrmaxiflemcom  11993  fz1f1o  12119  nndivdvds  12541  dvdsmultr2  12578  bitsmod  12701  pcmpt  13100  pcmpt2  13101  resrhm2b  14530  lssle0  14681  discld  15160  cncnpi  15252  cnptoprest2  15264  lmss  15270  txcn  15299  isxmet2d  15372  xblss2  15429  bdxmet  15525  xmetxp  15531  cncfcdm  15606  lgsneg  16057  lgsdilem  16060  2lgslem1a  16121  clwwlknonel  16587  clwwlknun  16596  eupth2lem2dc  16614