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  573  pm5.33  609  bianabs  611  baib  919  baibd  923  anxordi  1400  euan  2082  eueq3dc  2911  ifandc  3572  xpcom  5175  fvopab3g  5589  riota1a  5849  ctssdccl  7109  2omotaplemap  7255  recmulnqg  7389  ltexprlemloc  7605  mul0eqap  8626  eluz2  9533  rpnegap  9685  elfz2  10014  zmodid2  10351  shftfib  10831  dvdsssfz1  11857  modremain  11933  phisum  12239  ctiunctlemudc  12437  issubg  13031  resgrpisgrp  13053  issubrg  13340  txcnmpt  13743  reopnap  14008  ellimc3apf  14099