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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biantrur  303  biantrurd  305  anclb  319  pm5.42  320  pm5.32  457  anabs5  579  pm5.33  617  bianabs  619  annotanannot  680  baib  931  baibd  935  anxordi  1449  euan  2143  eueq3dc  3000  ifandc  3681  xpcom  5337  fvopab3g  5781  riota1a  6062  opabfi  7251  funisfsupp  7296  2omap  7324  ctssdccl  7457  2omotaplemap  7629  recmulnqg  7764  ltexprlemloc  7980  mul0eqap  9008  eluz2  9943  rpnegap  10104  elfz2  10435  zmodid2  10810  shftfib  11610  dvdsssfz1  12644  modremain  12721  ballotfilemdifcfz  13285  ctiunctlemudc  13386  issubg  14035  resgrpisgrp  14057  sscntz  14158  qusecsub  14225  issubrng  14616  issubrg  14638  txcnmpt  15499  reopnap  15772  ellimc3apf  15886  bpos  16320  ralrals  17356  ralals  17362