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

Theorem ibar 529
Description: Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.)
Assertion
Ref Expression
ibar (𝜑 → (𝜓 ↔ (𝜑𝜓)))

Proof of Theorem ibar
StepHypRef Expression
1 iba 528 . 2 (𝜑 → (𝜓 ↔ (𝜓𝜑)))
21biancomd 464 1 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  biantrurd  533  baib  536  baibd  540  bianabs  542  pm5.42  544  anclb  546  anabs5  659  annotanannot  831  pm5.33  832  pclem6  1020  moanimv  2672  moanim  2673  euan  2674  euanv  2678  ralanid  3135  rexanid  3216  eueq3  3638  reu6  3651  reuan  3808  ifan  4432  dfopif  4707  notzfaus  5153  reusv2lem5  5194  dmopab2rex  5672  fvopab3g  6630  riota1a  6996  dfom2  7438  suppssr  7712  mpocurryd  7786  boxcutc  8353  funisfsupp  8684  dfac3  9393  eluz2  12099  elixx3g  12601  elfz2  12749  zmodid2  13117  shftfib  14265  dvdsssfz1  15501  modremain  15592  sadadd2lem2  15632  smumullem  15674  issubg  18033  resgrpisgrp  18054  sscntz  18197  pgrpsubgsymgbi  18266  issubrg  19225  lindsmm  20654  mdetunilem8  20912  mdetunilem9  20913  cmpsub  21692  txcnmpt  21916  hausdiag  21937  fbfinnfr  22133  elfilss  22168  fixufil  22214  ibladdlem  24103  iblabslem  24111  cusgruvtxb  26887  usgr0edg0rusgr  27040  rgrusgrprc  27054  rusgrnumwwlkslem  27435  eclclwwlkn1  27541  eupth2lem1  27685  pjimai  29644  chrelati  29832  tltnle  30323  metidv  30749  satfv1lem  32217  dmopab3rexdif  32260  slenlt  32840  curf  34401  unccur  34406  cnambfre  34471  itg2addnclem2  34475  ibladdnclem  34479  iblabsnclem  34486  prjsprellsp  38758  expdiophlem1  39103  rfovcnvf1od  39835  fsovrfovd  39840  ntrneiel2  39921  odd2np1ALTV  43321  isrnghm  43641  rnghmval2  43644  uzlidlring  43678  islindeps  43988  elbigo2  44093
  Copyright terms: Public domain W3C validator