MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ibar Unicode version

Theorem ibar 491
Description: Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.)
Assertion
Ref Expression
ibar  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )

Proof of Theorem ibar
StepHypRef Expression
1 pm3.2 435 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
2 simpr 448 . 2  |-  ( (
ph  /\  ps )  ->  ps )
31, 2impbid1 195 1  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  biantrur  493  biantrurd  495  anclb  531  pm5.42  532  anabs5  785  pm5.33  849  bianabs  851  baib  872  baibd  876  pclem6  897  cad1  1404  euan  2288  eueq3  3045  ifan  3714  dfopif  3916  reusv2lem5  4661  dfom2  4780  fvopab3g  5734  riota1a  6498  boxcutc  7034  dfac3  7928  eluz2  10419  elixx3g  10854  elfz2  10975  shftfib  11807  sadadd2lem2  12882  smumullem  12924  issubg  14864  sscntz  15045  issubrg  15788  cmpsub  17378  txcnmpt  17570  fbfinnfr  17787  elfilss  17822  fixufil  17868  ibladdlem  19571  iblabslem  19579  sgmss  20749  cusgra2v  21330  eupath2lem1  21540  pjimai  23520  chrelati  23708  zmodid2  24886  wl-pm5.32  25936  itg2addnclem2  25951  ibladdnclem  25954  iblabsnclem  25961  divalgmodcl  26742  expdiophlem1  26776  lindsmm  26960  reuan  27619  frgra3v  27748
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator