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  4716  elrnmpt1  4896  fliftf  5821  elxp7  6196  eroveu  6653  sbthlemi5  6991  sbthlemi6  6992  elfi2  7002  reapltxor  8577  divap0b  8671  nnle1eq1  8974  nn0le0eq0  9235  nn0lt10b  9364  ioopos  9982  xrmaxiflemcom  11292  fz1f1o  11418  nndivdvds  11838  dvdsmultr2  11875  pcmpt  12378  pcmpt2  12379  lssle0  13705  discld  14113  cncnpi  14205  cnptoprest2  14217  lmss  14223  txcn  14252  isxmet2d  14325  xblss2  14382  bdxmet  14478  xmetxp  14484  cncfcdm  14546  lgsneg  14903  lgsdilem  14906