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  1411  euan  2101  eueq3dc  2938  ifandc  3600  xpcom  5217  fvopab3g  5637  riota1a  5900  opabfi  7008  ctssdccl  7186  2omotaplemap  7340  recmulnqg  7475  ltexprlemloc  7691  mul0eqap  8714  eluz2  9624  rpnegap  9778  elfz2  10107  zmodid2  10461  shftfib  11005  dvdsssfz1  12034  modremain  12111  ctiunctlemudc  12679  issubg  13379  resgrpisgrp  13401  qusecsub  13537  issubrng  13831  issubrg  13853  txcnmpt  14593  reopnap  14866  ellimc3apf  14980  2omap  15726