Theorem ibar 525

Description: Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.)

Assertion

Ref	Expression
ibar	|- ( ph -> ( ps <-> ( ph /\ ps ) ) )

Proof of Theorem ibar

Step	Hyp	Ref	Expression
1		pm3.2 463	. 2 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
2		simpr 477	. 2 |- ( ( ph /\ ps ) -> ps )
3	1, 2	impbid1 215	1 |- ( ph -> ( ps <-> ( ph /\ ps ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  biantrur  527  biantrurd  529  anclb  570  pm5.42  571  anabs5  851  pm5.33  922  bianabs  924  baib  944  baibd  948  pclem6  971  moanim  2529  euan  2530  eueq3  3381  reu6  3395  ifan  4134  dfopif  4399  reusv2lem5  4873  fvopab3g  6277  riota1a  6630  dfom2  7067  suppssr  7326  mpt2curryd  7395  boxcutc  7951  funisfsupp  8280  dfac3  8944  eluz2  11693  elixx3g  12188  elfz2  12333  zmodid2  12698  shftfib  13812  dvdsssfz1  15040  modremain  15132  sadadd2lem2  15172  smumullem  15214  issubg  17594  resgrpisgrp  17615  sscntz  17759  pgrpsubgsymgbi  17827  issubrg  18780  lindsmm  20167  mdetunilem8  20425  mdetunilem9  20426  cmpsub  21203  txcnmpt  21427  fbfinnfr  21645  elfilss  21680  fixufil  21726  ibladdlem  23586  iblabslem  23594  cusgruvtxb  26318  usgr0edg0rusgr  26471  rgrusgrprc  26485  rusgrnumwwlkslem  26864  eclclwwlksn1  26952  eupth2lem1  27078  pjimai  29035  chrelati  29223  tltnle  29662  metidv  29935  slenlt  31877  curf  33387  unccur  33392  cnambfre  33458  itg2addnclem2  33462  ibladdnclem  33466  iblabsnclem  33473  expdiophlem1  37588  rfovcnvf1od  38298  fsovrfovd  38303  ntrneiel2  38384  reuan  41180  odd2np1ALTV  41585  isrnghm  41892  rnghmval2  41895  uzlidlring  41929  islindeps  42242  elbigo2  42346