Theorem ibar 301

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 139	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
2		simpr 110	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3	1, 2	impbid1 142	1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biantrur  303  biantrurd  305  anclb  319  pm5.42  320  pm5.32  453  anabs5  575  pm5.33  613  bianabs  615  annotanannot  676  baib  927  baibd  931  anxordi  1445  euan  2136  eueq3dc  2981  ifandc  3650  xpcom  5290  fvopab3g  5728  riota1a  6002  opabfi  7175  ctssdccl  7353  2omotaplemap  7519  recmulnqg  7654  ltexprlemloc  7870  mul0eqap  8893  eluz2  9804  rpnegap  9964  elfz2  10293  zmodid2  10658  shftfib  11444  dvdsssfz1  12474  modremain  12551  ctiunctlemudc  13119  issubg  13821  resgrpisgrp  13843  qusecsub  13979  issubrng  14275  issubrg  14297  txcnmpt  15064  reopnap  15337  ellimc3apf  15451  2omap  16695