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 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biantrur  303  biantrurd  305  anclb  319  pm5.42  320  pm5.32  457  anabs5  579  pm5.33  617  bianabs  619  annotanannot  680  baib  931  baibd  935  anxordi  1449  euan  2143  eueq3dc  3000  ifandc  3681  xpcom  5334  fvopab3g  5778  riota1a  6059  opabfi  7247  funisfsupp  7291  2omap  7318  ctssdccl  7451  2omotaplemap  7623  recmulnqg  7758  ltexprlemloc  7974  mul0eqap  9001  eluz2  9929  rpnegap  10089  elfz2  10420  zmodid2  10791  shftfib  11590  dvdsssfz1  12621  modremain  12698  ballotfilemdifcfz  13229  ctiunctlemudc  13330  issubg  13978  resgrpisgrp  14000  qusecsub  14137  issubrng  14509  issubrg  14531  txcnmpt  15376  reopnap  15649  ellimc3apf  15763  ralrals  17161  ralals  17167