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  611  bianabs  613  baib  924  baibd  928  anxordi  1442  euan  2134  eueq3dc  2978  ifandc  3644  xpcom  5281  fvopab3g  5715  riota1a  5987  opabfi  7123  ctssdccl  7301  2omotaplemap  7466  recmulnqg  7601  ltexprlemloc  7817  mul0eqap  8840  eluz2  9751  rpnegap  9911  elfz2  10240  zmodid2  10604  shftfib  11374  dvdsssfz1  12403  modremain  12480  ctiunctlemudc  13048  issubg  13750  resgrpisgrp  13772  qusecsub  13908  issubrng  14203  issubrg  14225  txcnmpt  14987  reopnap  15260  ellimc3apf  15374  2omap  16530