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

Theorem ibar 524
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 462 . 2 (𝜑 → (𝜓 → (𝜑𝜓)))
2 simpr 476 . 2 ((𝜑𝜓) → 𝜓)
31, 2impbid1 214 1 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383
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 196  df-an 385
This theorem is referenced by:  biantrur  526  biantrurd  528  anclb  568  pm5.42  569  anabs5  847  pm5.33  918  bianabs  920  baib  942  baibd  946  pclem6  967  moanim  2517  euan  2518  eueq3  3348  reu6  3362  ifan  4084  dfopif  4337  reusv2lem5  4799  fvopab3g  6187  riota1a  6530  dfom2  6959  suppssr  7213  mpt2curryd  7282  boxcutc  7837  funisfsupp  8163  dfac3  8827  eluz2  11569  elixx3g  12059  elfz2  12204  zmodid2  12560  shftfib  13660  dvdsssfz1  14878  modremain  14970  sadadd2lem2  15010  smumullem  15052  issubg  17417  resgrpisgrp  17438  sscntz  17582  pgrpsubgsymgbi  17650  issubrg  18603  lindsmm  19986  mdetunilem8  20244  mdetunilem9  20245  cmpsub  21013  txcnmpt  21237  fbfinnfr  21455  elfilss  21490  fixufil  21536  ibladdlem  23392  iblabslem  23400  cusgra2v  25991  eclclwwlkn1  26359  el2wlkonotot  26400  rusgranumwlklem0  26475  eupath2lem1  26504  frgra3v  26529  pjimai  28419  chrelati  28607  tltnle  28993  metidv  29263  curf  32557  unccur  32562  cnambfre  32628  itg2addnclem2  32632  ibladdnclem  32636  iblabsnclem  32643  expdiophlem1  36606  rfovcnvf1od  37318  fsovrfovd  37323  ntrneiel2  37404  reuan  39829  odd2np1ALTV  40123  cusgruvtxb  40644  usgr0edg0rusgr  40775  rgrusgrprc  40789  eclclwwlksn1  41259  eupth2lem1  41386  isrnghm  41682  rnghmval2  41685  uzlidlring  41719  islindeps  42036  elbigo2  42144
  Copyright terms: Public domain W3C validator