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  2978  ifandc  3644  xpcom  5281  fvopab3g  5715  riota1a  5987  opabfi  7126  ctssdccl  7304  2omotaplemap  7469  recmulnqg  7604  ltexprlemloc  7820  mul0eqap  8843  eluz2  9754  rpnegap  9914  elfz2  10243  zmodid2  10607  shftfib  11377  dvdsssfz1  12406  modremain  12483  ctiunctlemudc  13051  issubg  13753  resgrpisgrp  13775  qusecsub  13911  issubrng  14206  issubrg  14228  txcnmpt  14990  reopnap  15263  ellimc3apf  15377  2omap  16544