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

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

Proof of Theorem ibar
StepHypRef Expression
1 pm3.2 463 . 2 (𝜑 → (𝜓 → (𝜑𝜓)))
2 simpr 477 . 2 ((𝜑𝜓) → 𝜓)
31, 2impbid1 215 1 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384 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 197  df-an 386 This theorem is referenced by:  biantrur  527  biantrurd  529  anclb  569  pm5.42  570  anabs5  850  pm5.33  921  bianabs  923  baib  943  baibd  947  pclem6  970  moanim  2528  euan  2529  eueq3  3367  reu6  3381  ifan  4111  dfopif  4372  reusv2lem5  4838  fvopab3g  6239  riota1a  6590  dfom2  7021  suppssr  7278  mpt2curryd  7347  boxcutc  7903  funisfsupp  8232  dfac3  8896  eluz2  11645  elixx3g  12138  elfz2  12283  zmodid2  12646  shftfib  13754  dvdsssfz1  14975  modremain  15067  sadadd2lem2  15107  smumullem  15149  issubg  17526  resgrpisgrp  17547  sscntz  17691  pgrpsubgsymgbi  17759  issubrg  18712  lindsmm  20099  mdetunilem8  20357  mdetunilem9  20358  cmpsub  21126  txcnmpt  21350  fbfinnfr  21568  elfilss  21603  fixufil  21649  ibladdlem  23509  iblabslem  23517  cusgruvtxb  26222  usgr0edg0rusgr  26358  rgrusgrprc  26372  rusgrnumwwlkslem  26748  eclclwwlksn1  26835  eupth2lem1  26961  pjimai  28905  chrelati  29093  tltnle  29471  metidv  29741  curf  33054  unccur  33059  cnambfre  33125  itg2addnclem2  33129  ibladdnclem  33133  iblabsnclem  33140  expdiophlem1  37103  rfovcnvf1od  37815  fsovrfovd  37820  ntrneiel2  37901  reuan  40510  odd2np1ALTV  40910  isrnghm  41206  rnghmval2  41209  uzlidlring  41243  islindeps  41556  elbigo2  41664
 Copyright terms: Public domain W3C validator