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  2098  eueq3dc  2935  ifandc  3596  xpcom  5213  fvopab3g  5631  riota1a  5894  opabfi  6994  ctssdccl  7172  2omotaplemap  7319  recmulnqg  7453  ltexprlemloc  7669  mul0eqap  8691  eluz2  9601  rpnegap  9755  elfz2  10084  zmodid2  10426  shftfib  10970  dvdsssfz1  11997  modremain  12073  phisum  12381  ctiunctlemudc  12597  issubg  13246  resgrpisgrp  13268  qusecsub  13404  issubrng  13698  issubrg  13720  txcnmpt  14452  reopnap  14725  ellimc3apf  14839