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	⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))

Proof of Theorem ibar

Step	Hyp	Ref	Expression
1		pm3.2 138	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
2		simpr 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3	1, 2	impbid1 141	1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))

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  448  anabs5  562  pm5.33  598  bianabs  600  baib  904  baibd  908  anxordi  1378  euan  2055  eueq3dc  2858  ifandc  3508  xpcom  5085  fvopab3g  5494  riota1a  5749  ctssdccl  6996  recmulnqg  7199  ltexprlemloc  7415  mul0eqap  8431  eluz2  9332  rpnegap  9474  elfz2  9797  zmodid2  10125  shftfib  10595  dvdsssfz1  11550  modremain  11626  ctiunctlemudc  11950  txcnmpt  12442  reopnap  12707  ellimc3apf  12798