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  609  bianabs  611  baib  920  baibd  924  anxordi  1411  euan  2101  eueq3dc  2938  ifandc  3599  xpcom  5216  fvopab3g  5634  riota1a  5897  opabfi  6999  ctssdccl  7177  2omotaplemap  7324  recmulnqg  7458  ltexprlemloc  7674  mul0eqap  8697  eluz2  9607  rpnegap  9761  elfz2  10090  zmodid2  10444  shftfib  10988  dvdsssfz1  12017  modremain  12094  ctiunctlemudc  12654  issubg  13303  resgrpisgrp  13325  qusecsub  13461  issubrng  13755  issubrg  13777  txcnmpt  14509  reopnap  14782  ellimc3apf  14896