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  5278  fvopab3g  5712  riota1a  5984  opabfi  7116  ctssdccl  7294  2omotaplemap  7459  recmulnqg  7594  ltexprlemloc  7810  mul0eqap  8833  eluz2  9744  rpnegap  9899  elfz2  10228  zmodid2  10591  shftfib  11355  dvdsssfz1  12384  modremain  12461  ctiunctlemudc  13029  issubg  13731  resgrpisgrp  13753  qusecsub  13889  issubrng  14184  issubrg  14206  txcnmpt  14968  reopnap  15241  ellimc3apf  15355  2omap  16472