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  3563  xpcom  5157  fvopab3g  5569  riota1a  5828  ctssdccl  7088  recmulnqg  7353  ltexprlemloc  7569  mul0eqap  8588  eluz2  9493  rpnegap  9643  elfz2  9972  zmodid2  10308  shftfib  10787  dvdsssfz1  11812  modremain  11888  phisum  12194  ctiunctlemudc  12392  txcnmpt  13067  reopnap  13332  ellimc3apf  13423