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  453  anabs5  573  pm5.33  609  bianabs  611  baib  921  baibd  925  anxordi  1420  euan  2110  eueq3dc  2947  ifandc  3610  xpcom  5230  fvopab3g  5654  riota1a  5921  opabfi  7037  ctssdccl  7215  2omotaplemap  7371  recmulnqg  7506  ltexprlemloc  7722  mul0eqap  8745  eluz2  9656  rpnegap  9810  elfz2  10139  zmodid2  10499  shftfib  11167  dvdsssfz1  12196  modremain  12273  ctiunctlemudc  12841  issubg  13542  resgrpisgrp  13564  qusecsub  13700  issubrng  13994  issubrg  14016  txcnmpt  14778  reopnap  15051  ellimc3apf  15165  2omap  15969