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  575  pm5.33  613  bianabs  615  annotanannot  676  baib  927  baibd  931  anxordi  1445  euan  2139  eueq3dc  2994  ifandc  3667  xpcom  5314  fvopab3g  5755  riota1a  6032  opabfi  7213  funisfsupp  7257  2omap  7282  ctssdccl  7415  2omotaplemap  7587  recmulnqg  7722  ltexprlemloc  7938  mul0eqap  8961  eluz2  9877  rpnegap  10037  elfz2  10368  zmodid2  10738  shftfib  11533  dvdsssfz1  12563  modremain  12640  ballotfilemdifcfz  13171  ctiunctlemudc  13272  issubg  13974  resgrpisgrp  13996  qusecsub  14132  issubrng  14430  issubrg  14452  txcnmpt  15250  reopnap  15523  ellimc3apf  15637