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  2139  eueq3dc  2994  ifandc  3667  xpcom  5314  fvopab3g  5755  riota1a  6032  opabfi  7213  funisfsupp  7257  2omap  7282  ctssdccl  7415  2omotaplemap  7587  recmulnqg  7722  ltexprlemloc  7938  mul0eqap  8964  eluz2  9880  rpnegap  10040  elfz2  10371  zmodid2  10741  shftfib  11536  dvdsssfz1  12567  modremain  12644  ballotfilemdifcfz  13175  ctiunctlemudc  13276  issubg  13930  resgrpisgrp  13952  qusecsub  14088  issubrng  14449  issubrg  14471  txcnmpt  15268  reopnap  15541  ellimc3apf  15655