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  611  bianabs  613  baib  924  baibd  928  anxordi  1442  euan  2134  eueq3dc  2977  ifandc  3643  xpcom  5271  fvopab3g  5700  riota1a  5968  opabfi  7088  ctssdccl  7266  2omotaplemap  7431  recmulnqg  7566  ltexprlemloc  7782  mul0eqap  8805  eluz2  9716  rpnegap  9870  elfz2  10199  zmodid2  10561  shftfib  11320  dvdsssfz1  12349  modremain  12426  ctiunctlemudc  12994  issubg  13696  resgrpisgrp  13718  qusecsub  13854  issubrng  14148  issubrg  14170  txcnmpt  14932  reopnap  15205  ellimc3apf  15319  2omap  16290