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  2977  ifandc  3643  xpcom  5275  fvopab3g  5707  riota1a  5975  opabfi  7100  ctssdccl  7278  2omotaplemap  7443  recmulnqg  7578  ltexprlemloc  7794  mul0eqap  8817  eluz2  9728  rpnegap  9882  elfz2  10211  zmodid2  10574  shftfib  11334  dvdsssfz1  12363  modremain  12440  ctiunctlemudc  13008  issubg  13710  resgrpisgrp  13732  qusecsub  13868  issubrng  14163  issubrg  14185  txcnmpt  14947  reopnap  15220  ellimc3apf  15334  2omap  16359