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  920  baibd  924  anxordi  1410  euan  2092  eueq3dc  2923  ifandc  3584  xpcom  5187  fvopab3g  5602  riota1a  5863  ctssdccl  7124  2omotaplemap  7270  recmulnqg  7404  ltexprlemloc  7620  mul0eqap  8641  eluz2  9548  rpnegap  9700  elfz2  10029  zmodid2  10366  shftfib  10846  dvdsssfz1  11872  modremain  11948  phisum  12254  ctiunctlemudc  12452  issubg  13065  resgrpisgrp  13087  qusecsub  13166  issubrng  13419  issubrg  13441  txcnmpt  14069  reopnap  14334  ellimc3apf  14425