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  920  baibd  924  anxordi  1411  euan  2098  eueq3dc  2934  ifandc  3595  xpcom  5212  fvopab3g  5630  riota1a  5893  opabfi  6992  ctssdccl  7170  2omotaplemap  7317  recmulnqg  7451  ltexprlemloc  7667  mul0eqap  8689  eluz2  9598  rpnegap  9752  elfz2  10081  zmodid2  10423  shftfib  10967  dvdsssfz1  11994  modremain  12070  phisum  12378  ctiunctlemudc  12594  issubg  13243  resgrpisgrp  13265  qusecsub  13401  issubrng  13695  issubrg  13717  txcnmpt  14441  reopnap  14706  ellimc3apf  14814