Theorem ibar 285

Description: Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.) (Revised by NM, 24-Mar-2013.)

Assertion

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

Proof of Theorem ibar

Step	Hyp	Ref	Expression
1		pm3.2 126	. 2 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
2		simpr 103	. 2 |- ( ( ph /\ ps ) -> ps )
3	1, 2	impbid1 130	1 |- ( ph -> ( ps <-> ( ph /\ ps ) ) )

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  biantrur  287  biantrurd  289  anclb  302  pm5.42  303  pm5.32  426  anabs5  507  pm5.33  541  bianabs  543  baib  828  baibd  832  anxordi  1291  euan  1956  eueq3dc  2715  xpcom  4864  fvopab3g  5245  riota1a  5487  recmulnqg  6489  ltexprlemloc  6705  eluz2  8479  rpnegap  8615  elfz2  8881  shftfib  9424