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  449  anabs5  563  pm5.33  599  bianabs  601  baib  909  baibd  913  anxordi  1390  euan  2070  eueq3dc  2900  ifandc  3557  xpcom  5150  fvopab3g  5559  riota1a  5817  ctssdccl  7076  recmulnqg  7332  ltexprlemloc  7548  mul0eqap  8567  eluz2  9472  rpnegap  9622  elfz2  9951  zmodid2  10287  shftfib  10765  dvdsssfz1  11790  modremain  11866  phisum  12172  ctiunctlemudc  12370  txcnmpt  12913  reopnap  13178  ellimc3apf  13269