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  575  pm5.33  613  bianabs  615  baib  926  baibd  930  anxordi  1444  euan  2136  eueq3dc  2980  ifandc  3646  xpcom  5283  fvopab3g  5719  riota1a  5992  opabfi  7132  ctssdccl  7310  2omotaplemap  7476  recmulnqg  7611  ltexprlemloc  7827  mul0eqap  8850  eluz2  9761  rpnegap  9921  elfz2  10250  zmodid2  10614  shftfib  11384  dvdsssfz1  12414  modremain  12491  ctiunctlemudc  13059  issubg  13761  resgrpisgrp  13783  qusecsub  13919  issubrng  14215  issubrg  14237  txcnmpt  14999  reopnap  15272  ellimc3apf  15386  2omap  16597