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  5275  fvopab3g  5709  riota1a  5981  opabfi  7108  ctssdccl  7286  2omotaplemap  7451  recmulnqg  7586  ltexprlemloc  7802  mul0eqap  8825  eluz2  9736  rpnegap  9890  elfz2  10219  zmodid2  10582  shftfib  11342  dvdsssfz1  12371  modremain  12448  ctiunctlemudc  13016  issubg  13718  resgrpisgrp  13740  qusecsub  13876  issubrng  14171  issubrg  14193  txcnmpt  14955  reopnap  15228  ellimc3apf  15342  2omap  16388