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  2200  eueq3  2940  ifan  3604  dfopif  3793  reusv2lem5  4539  dfom2  4658  fvopab3g  5598  riota1a  6324  boxcutc  6859  dfac3  7748  eluz2  10236  elixx3g  10669  elfz2  10789  shftfib  11567  sadadd2lem2  12641  smumullem  12683  issubg  14621  sscntz  14802  issubrg  15545  cmpsub  17127  txcnmpt  17318  fbfinnfr  17536  elfilss  17571  fixufil  17617  ibladdlem  19174  iblabslem  19182  sgmss  20344  pjimai  22756  chrelati  22944  eupath2lem1  23901  zmodid2  24010  wl-pm5.32  24919  cmppar3  25974  divalgmodcl  27080  expdiophlem1  27114  lindsmm  27298  reuan  27958  cusgra2v  28158  frgra3v  28180
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