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  5709  riota1a  5981  opabfi  7111  ctssdccl  7289  2omotaplemap  7454  recmulnqg  7589  ltexprlemloc  7805  mul0eqap  8828  eluz2  9739  rpnegap  9894  elfz2  10223  zmodid2  10586  shftfib  11350  dvdsssfz1  12379  modremain  12456  ctiunctlemudc  13024  issubg  13726  resgrpisgrp  13748  qusecsub  13884  issubrng  14179  issubrg  14201  txcnmpt  14963  reopnap  15236  ellimc3apf  15350  2omap  16446