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

Theorem ibar 490
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 434 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
2 simpr 447 . 2  |-  ( (
ph  /\  ps )  ->  ps )
31, 2impbid1 194 1  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  biantrur  492  biantrurd  494  anclb  530  pm5.42  531  anabs5  784  pm5.33  848  bianabs  850  baib  871  baibd  875  pclem6  896  cad1  1388  euan  2213  eueq3  2953  ifan  3617  dfopif  3809  reusv2lem5  4555  dfom2  4674  fvopab3g  5614  riota1a  6340  boxcutc  6875  dfac3  7764  eluz2  10252  elixx3g  10685  elfz2  10805  shftfib  11583  sadadd2lem2  12657  smumullem  12699  issubg  14637  sscntz  14818  issubrg  15561  cmpsub  17143  txcnmpt  17334  fbfinnfr  17552  elfilss  17587  fixufil  17633  ibladdlem  19190  iblabslem  19198  sgmss  20360  pjimai  22772  chrelati  22960  eupath2lem1  23916  zmodid2  24025  wl-pm5.32  24991  itg2addnclem2  25004  ibladdnclem  25007  iblabsnclem  25014  cmppar3  26077  divalgmodcl  27183  expdiophlem1  27217  lindsmm  27401  reuan  28061  cusgra2v  28297  frgra3v  28426
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 177  df-an 360
  Copyright terms: Public domain W3C validator