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  2137  eueq3dc  2990  ifandc  3662  xpcom  5308  fvopab3g  5749  riota1a  6023  opabfi  7199  funisfsupp  7243  2omap  7268  ctssdccl  7401  2omotaplemap  7570  recmulnqg  7705  ltexprlemloc  7921  mul0eqap  8943  eluz2  9858  rpnegap  10018  elfz2  10348  zmodid2  10713  shftfib  11504  dvdsssfz1  12534  modremain  12611  ctiunctlemudc  13180  issubg  13882  resgrpisgrp  13904  qusecsub  14040  issubrng  14336  issubrg  14358  txcnmpt  15130  reopnap  15403  ellimc3apf  15517