Theorem ibar 299

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 138	. 2 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
2		simpr 109	. 2 |- ( ( ph /\ ps ) -> ps )
3	1, 2	impbid1 141	1 |- ( ph -> ( ps <-> ( ph /\ ps ) ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biantrur  301  biantrurd  303  anclb  317  pm5.42  318  pm5.32  449  anabs5  563  pm5.33  599  bianabs  601  baib  905  baibd  909  anxordi  1379  euan  2056  eueq3dc  2862  ifandc  3513  xpcom  5093  fvopab3g  5502  riota1a  5757  ctssdccl  7004  recmulnqg  7223  ltexprlemloc  7439  mul0eqap  8455  eluz2  9356  rpnegap  9503  elfz2  9828  zmodid2  10156  shftfib  10627  dvdsssfz1  11586  modremain  11662  ctiunctlemudc  11986  txcnmpt  12481  reopnap  12746  ellimc3apf  12837