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	|- ( ph -> ( ps <-> ( ph /\ ps ) ) )

Proof of Theorem ibar

Step	Hyp	Ref	Expression
1		pm3.2 139	. 2 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
2		simpr 110	. 2 |- ( ( ph /\ ps ) -> ps )
3	1, 2	impbid1 142	1 |- ( ph -> ( ps <-> ( ph /\ ps ) ) )

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  457  anabs5  579  pm5.33  617  bianabs  619  annotanannot  680  baib  931  baibd  935  anxordi  1449  euan  2143  eueq3dc  3000  ifandc  3678  xpcom  5329  fvopab3g  5772  riota1a  6049  opabfi  7237  funisfsupp  7281  2omap  7308  ctssdccl  7441  2omotaplemap  7613  recmulnqg  7748  ltexprlemloc  7964  mul0eqap  8990  eluz2  9906  rpnegap  10066  elfz2  10397  zmodid2  10767  shftfib  11566  dvdsssfz1  12597  modremain  12674  ballotfilemdifcfz  13205  ctiunctlemudc  13306  issubg  13953  resgrpisgrp  13975  qusecsub  14112  issubrng  14480  issubrg  14502  txcnmpt  15297  reopnap  15570  ellimc3apf  15684