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  5229  fvopab3g  5652  riota1a  5919  opabfi  7035  ctssdccl  7213  2omotaplemap  7369  recmulnqg  7504  ltexprlemloc  7720  mul0eqap  8743  eluz2  9654  rpnegap  9808  elfz2  10137  zmodid2  10497  shftfib  11134  dvdsssfz1  12163  modremain  12240  ctiunctlemudc  12808  issubg  13509  resgrpisgrp  13531  qusecsub  13667  issubrng  13961  issubrg  13983  txcnmpt  14745  reopnap  15018  ellimc3apf  15132  2omap  15932