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  4804  elrnmpt1  4989  fliftf  5950  elxp7  6342  eroveu  6838  sbthlemi5  7203  sbthlemi6  7204  elfi2  7214  sspw1or2  7446  reapltxor  8811  divap0b  8905  nnle1eq1  9209  nn0le0eq0  9472  nn0lt10b  9604  ioopos  10229  xrmaxiflemcom  11872  fz1f1o  11998  nndivdvds  12420  dvdsmultr2  12457  bitsmod  12580  pcmpt  12979  pcmpt2  12980  resrhm2b  14327  lssle0  14451  discld  14930  cncnpi  15022  cnptoprest2  15034  lmss  15040  txcn  15069  isxmet2d  15142  xblss2  15199  bdxmet  15295  xmetxp  15301  cncfcdm  15376  lgsneg  15826  lgsdilem  15829  2lgslem1a  15890  clwwlknonel  16356  clwwlknun  16365  eupth2lem2dc  16383