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  4735  elrnmpt1  4917  fliftf  5846  elxp7  6228  eroveu  6685  sbthlemi5  7027  sbthlemi6  7028  elfi2  7038  reapltxor  8616  divap0b  8710  nnle1eq1  9014  nn0le0eq0  9277  nn0lt10b  9406  ioopos  10025  xrmaxiflemcom  11414  fz1f1o  11540  nndivdvds  11961  dvdsmultr2  11998  pcmpt  12512  pcmpt2  12513  resrhm2b  13805  lssle0  13928  discld  14372  cncnpi  14464  cnptoprest2  14476  lmss  14482  txcn  14511  isxmet2d  14584  xblss2  14641  bdxmet  14737  xmetxp  14743  cncfcdm  14818  lgsneg  15265  lgsdilem  15268  2lgslem1a  15329