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  5337  fvopab3g  5781  riota1a  6062  opabfi  7252  funisfsupp  7297  2omap  7325  ctssdccl  7458  2omotaplemap  7630  recmulnqg  7765  ltexprlemloc  7981  mul0eqap  9009  eluz2  9944  rpnegap  10105  elfz2  10436  zmodid2  10811  shftfib  11611  dvdsssfz1  12645  modremain  12722  ballotfilemdifcfz  13286  ctiunctlemudc  13387  issubg  14036  resgrpisgrp  14058  sscntz  14159  qusecsub  14226  issubrng  14617  issubrg  14639  txcnmpt  15511  reopnap  15784  ellimc3apf  15898  bpos  16332  ralrals  17368  ralals  17374