Theorem biantrud 300

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 296	. 2 |- ( ps -> ( ch <-> ( ch /\ ps ) ) )
3	1, 2	syl 14	1 |- ( ph -> ( ch <-> ( ch /\ ps ) ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbiran2d  436  posng  4571  elrnmpt1  4750  fliftf  5654  elxp7  6022  eroveu  6474  sbthlemi5  6801  sbthlemi6  6802  elfi2  6812  reapltxor  8266  divap0b  8353  nnle1eq1  8651  nn0le0eq0  8906  nn0lt10b  9032  ioopos  9623  xrmaxiflemcom  10907  fz1f1o  11033  nndivdvds  11344  dvdsmultr2  11378  discld  12145  cncnpi  12236  cnptoprest2  12248  lmss  12254  txcn  12283  isxmet2d  12334  xblss2  12391  bdxmet  12487  xmetxp  12493  cncffvrn  12552