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

Theorem ibar 511
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 453 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
2 simpr 467 . 2  |-  ( (
ph  /\  ps )  ->  ps )
31, 2impbid1 208 1  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  biantrur  513  biantrurd  515  anclb  554  pm5.42  555  anabs5  823  pm5.33  894  bianabs  896  baib  919  baibd  925  pclem6  946  moanim  2369  euan  2370  eueq3  3225  ifan  3939  dfopif  4177  reusv2lem5  4622  fvopab3g  5967  riota1a  6296  dfom2  6721  suppssr  6973  mpt2curryd  7042  boxcutc  7591  funisfsupp  7914  dfac3  8578  eluz2  11194  elixx3g  11677  elfz2  11820  zmodid2  12157  shftfib  13184  sadadd2lem2  14473  smumullem  14515  issubg  16866  resgrpisgrp  16887  sscntz  17029  pgrpsubgsymgbi  17097  issubrg  18057  lindsmm  19435  mdetunilem8  19693  mdetunilem9  19694  cmpsub  20464  txcnmpt  20688  fbfinnfr  20905  elfilss  20940  fixufil  20986  ibladdlem  22826  iblabslem  22834  sgmss  24082  cusgra2v  25239  eclclwwlkn1  25609  el2wlkonotot  25650  rusgranumwlklem0  25725  eupath2lem1  25754  frgra3v  25779  pjimai  27878  chrelati  28066  tltnle  28472  metidv  28744  cnambfre  32034  itg2addnclem2  32039  ibladdnclem  32043  iblabsnclem  32050  divalgmodcl  35887  expdiophlem1  35921  reuan  38639  odd2np1ALTV  38841  cusgruvtxb  39540  usgr0edg0rusgr  39641  rgrusgrprc  39654  isspthonpth-av  39781  isrnghm  40165  rnghmval2  40168  uzlidlring  40202  islindeps  40519  elbigo2  40636
  Copyright terms: Public domain W3C validator