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  575  pm5.33  613  bianabs  615  annotanannot  676  baib  927  baibd  931  anxordi  1445  euan  2137  eueq3dc  2991  ifandc  3663  xpcom  5309  fvopab3g  5750  riota1a  6024  opabfi  7200  funisfsupp  7244  2omap  7269  ctssdccl  7402  2omotaplemap  7571  recmulnqg  7706  ltexprlemloc  7922  mul0eqap  8944  eluz2  9859  rpnegap  10019  elfz2  10349  zmodid2  10714  shftfib  11508  dvdsssfz1  12538  modremain  12615  ctiunctlemudc  13188  issubg  13890  resgrpisgrp  13912  qusecsub  14048  issubrng  14344  issubrg  14366  txcnmpt  15138  reopnap  15411  ellimc3apf  15525