Theorem ibar 295

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 137	. 2 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
2		simpr 108	. 2 |- ( ( ph /\ ps ) -> ps )
3	1, 2	impbid1 140	1 |- ( ph -> ( ps <-> ( ph /\ ps ) ) )

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  biantrur  297  biantrurd  299  anclb  312  pm5.42  313  pm5.32  440  anabs5  537  pm5.33  573  bianabs  575  baib  861  baibd  865  anxordi  1331  euan  1997  eueq3dc  2766  xpcom  4884  fvopab3g  5266  riota1a  5507  recmulnqg  6581  ltexprlemloc  6797  eluz2  8625  rpnegap  8766  elfz2  9036  zmodid2  9354  shftfib  9711  dvdsssfz1  10252  modremain  10329