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  2112  eueq3dc  2954  ifandc  3620  xpcom  5248  fvopab3g  5675  riota1a  5942  opabfi  7061  ctssdccl  7239  2omotaplemap  7404  recmulnqg  7539  ltexprlemloc  7755  mul0eqap  8778  eluz2  9689  rpnegap  9843  elfz2  10172  zmodid2  10534  shftfib  11249  dvdsssfz1  12278  modremain  12355  ctiunctlemudc  12923  issubg  13624  resgrpisgrp  13646  qusecsub  13782  issubrng  14076  issubrg  14098  txcnmpt  14860  reopnap  15133  ellimc3apf  15247  2omap  16132