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  450  anabs5  568  pm5.33  604  bianabs  606  baib  914  baibd  918  anxordi  1395  euan  2075  eueq3dc  2904  ifandc  3562  xpcom  5155  fvopab3g  5567  riota1a  5826  ctssdccl  7085  recmulnqg  7342  ltexprlemloc  7558  mul0eqap  8577  eluz2  9482  rpnegap  9632  elfz2  9961  zmodid2  10297  shftfib  10776  dvdsssfz1  11801  modremain  11877  phisum  12183  ctiunctlemudc  12381  txcnmpt  13028  reopnap  13293  ellimc3apf  13384