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  7342  recmulnqg  7477  ltexprlemloc  7693  mul0eqap  8716  eluz2  9626  rpnegap  9780  elfz2  10109  zmodid2  10463  shftfib  11007  dvdsssfz1  12036  modremain  12113  ctiunctlemudc  12681  issubg  13381  resgrpisgrp  13403  qusecsub  13539  issubrng  13833  issubrg  13855  txcnmpt  14617  reopnap  14890  ellimc3apf  15004  2omap  15750