Theorem ibar 642

Description: Introduction of antecedent as conjunct.

Assertion

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

Proof of Theorem ibar

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

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  pm5.33 649  pm5.42 651  bianabs 652  baib 684  biantrur 724  iunconst 2569  dfom2 3130  fvopab3 3774  aceq3 4720  ltxrltt 5487  elioo3g 6335  eluz2t 6371  elfz2t 6422  iscld2 7649  elbl2 7820  metcn4 7954  h2hcau 8833  h2hlm 8834  elnlfnt 9843  chrelat 10282  ompfl3 10420  subsp 10523  ismonb1 10688

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 147  df-an 225

Copyright terms: Public domain