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  575  pm5.33  613  bianabs  615  baib  926  baibd  930  anxordi  1444  euan  2136  eueq3dc  2980  ifandc  3646  xpcom  5283  fvopab3g  5719  riota1a  5991  opabfi  7131  ctssdccl  7309  2omotaplemap  7475  recmulnqg  7610  ltexprlemloc  7826  mul0eqap  8849  eluz2  9760  rpnegap  9920  elfz2  10249  zmodid2  10613  shftfib  11383  dvdsssfz1  12412  modremain  12489  ctiunctlemudc  13057  issubg  13759  resgrpisgrp  13781  qusecsub  13917  issubrng  14212  issubrg  14234  txcnmpt  14996  reopnap  15269  ellimc3apf  15383  2omap  16594