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  442  posng  4791  elrnmpt1  4975  fliftf  5929  elxp7  6322  eroveu  6781  sbthlemi5  7139  sbthlemi6  7140  elfi2  7150  reapltxor  8747  divap0b  8841  nnle1eq1  9145  nn0le0eq0  9408  nn0lt10b  9538  ioopos  10158  xrmaxiflemcom  11775  fz1f1o  11901  nndivdvds  12322  dvdsmultr2  12359  bitsmod  12482  pcmpt  12881  pcmpt2  12882  resrhm2b  14228  lssle0  14351  discld  14825  cncnpi  14917  cnptoprest2  14929  lmss  14935  txcn  14964  isxmet2d  15037  xblss2  15094  bdxmet  15190  xmetxp  15196  cncfcdm  15271  lgsneg  15718  lgsdilem  15721  2lgslem1a  15782