Theorem ibar 646

Description: Introduction of antecedent as conjunct.

Assertion

Ref	Expression
ibar	|- (ph -> (ps <-> (ph /\ ps)))

Proof of Theorem ibar

Step	Hyp	Ref	Expression
1		anclb 327	. 2 |- ((ph -> ps) <-> (ph -> (ph /\ ps)))
2	1	pm5.74ri 590	1 |- (ph -> (ps <-> (ph /\ ps)))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221

This theorem is referenced by:  pm5.33 653  pm5.42 655  bianabs 656  baib 689  biantrur 730  iunconst 2640  dfom2 3220  fvopab3 3888  aceq3 4879  ltxrlt 5654  elioo3g 6506  eluz2 6548  elfz2 6600  iscld2 7880  elbl2 8049  metcn4 8182  h2hcau 9124  h2hlm 9125  elnlfn 10132  chrelati 10572  ompfl3 10712  subsp 11056  ismonb1 11266  isepib1 11276  cncls 11473  cnntr 11474  compsub 11488  topbasfne 11560  fbaslim 11680  limfilcf 11683  isflimf 11709  flimfnei 11710  flimfbas 11713  isfclus 11718  fclusbas 11722  flimfcls 11725

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145  df-an 223

Copyright terms: Public domain