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  457  anabs5  579  pm5.33  617  bianabs  619  annotanannot  680  baib  931  baibd  935  anxordi  1449  euan  2143  eueq3dc  3000  ifandc  3681  xpcom  5332  fvopab3g  5775  riota1a  6053  opabfi  7241  funisfsupp  7285  2omap  7312  ctssdccl  7445  2omotaplemap  7617  recmulnqg  7752  ltexprlemloc  7968  mul0eqap  8994  eluz2  9910  rpnegap  10070  elfz2  10401  zmodid2  10772  shftfib  11571  dvdsssfz1  12602  modremain  12679  ballotfilemdifcfz  13210  ctiunctlemudc  13311  issubg  13959  resgrpisgrp  13981  qusecsub  14118  issubrng  14490  issubrg  14512  txcnmpt  15357  reopnap  15630  ellimc3apf  15744  ralrals  17123  ralals  17129