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  921  baibd  925  anxordi  1420  euan  2111  eueq3dc  2951  ifandc  3614  xpcom  5237  fvopab3g  5664  riota1a  5931  opabfi  7049  ctssdccl  7227  2omotaplemap  7384  recmulnqg  7519  ltexprlemloc  7735  mul0eqap  8758  eluz2  9669  rpnegap  9823  elfz2  10152  zmodid2  10514  shftfib  11204  dvdsssfz1  12233  modremain  12310  ctiunctlemudc  12878  issubg  13579  resgrpisgrp  13601  qusecsub  13737  issubrng  14031  issubrg  14053  txcnmpt  14815  reopnap  15088  ellimc3apf  15202  2omap  16067