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

Theorem pm5.32i 668
Description: Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.)
Hypothesis
Ref Expression
pm5.32i.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
pm5.32i ((𝜑𝜓) ↔ (𝜑𝜒))

Proof of Theorem pm5.32i
StepHypRef Expression
1 pm5.32i.1 . 2 (𝜑 → (𝜓𝜒))
2 pm5.32 667 . 2 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ↔ (𝜑𝜒)))
31, 2mpbi 220 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:  pm5.32ri  669  biadan2  673  anbi2i  729  abai  835  anabs5  850  pm5.33  921  cases  991  equsexvw  1929  equsexv  2106  equsexALT  2293  2sb5rf  2450  2eu8  2559  eq2tri  2682  rexbiia  3035  reubiia  3120  rmobiia  3125  rabbiia  3177  ceqsrexbv  3325  euxfr  3379  2reu5  3403  dfpss3  3677  eldifpr  4182  eldiftp  4206  eldifsn  4294  elrint  4490  elriin  4566  reuxfrd  4863  opeqsn  4937  rabxp  5124  copsex2gb  5201  eliunxp  5229  restidsing  5427  ressn  5640  dflim2  5750  fncnv  5930  dff1o5  6113  respreima  6310  dff4  6339  dffo3  6340  f1ompt  6348  fsn  6367  fconst3  6442  fconst4  6443  eufnfv  6456  dff13  6477  f1mpt  6483  isocnv3  6547  isores2  6548  isoini  6553  eloprabga  6712  mpt2mptx  6716  resoprab  6721  elrnmpt2res  6739  ov6g  6763  dfwe2  6943  dflim3  7009  dflim4  7010  dfopab2  7182  dfoprab3s  7183  dfoprab3  7184  fparlem1  7237  fparlem2  7238  brtpos2  7318  dftpos3  7330  tpostpos  7332  dfsmo2  7404  dfrecs3  7429  tz7.48-1  7498  ondif1  7541  ondif2  7542  elixp2  7872  mapsnen  7995  xpcomco  8010  eqinf  8350  infempty  8372  r0weon  8795  isinfcard  8875  dfac5lem1  8906  fpwwe  9428  axgroth6  9610  axgroth3  9613  elni2  9659  indpi  9689  recmulnq  9746  genpass  9791  lemul1a  10837  sup3  10940  elnn0z  11350  elznn0  11352  elznn  11353  eluz2b1  11719  eluz2b3  11722  elfz2nn0  12388  elfzo3  12443  shftidt2  13771  clim0  14187  fprod2dlem  14654  divalglem4  15062  ndvdsadd  15077  gcdaddmlem  15188  algfx  15236  isprm3  15339  isprm5  15362  isprm7  15363  xpsfrnel  16163  isacs2  16254  isfull2  16511  isfth2  16515  tosso  16976  odudlatb  17136  nsgacs  17570  isgim2  17647  isabl2  18141  iscyg3  18228  iscrng2  18503  isdrng2  18697  drngprop  18698  islmim2  19006  islpir2  19191  isnzr2  19203  iunocv  19965  ishil2  20003  islinds2  20092  ssntr  20802  isclo2  20832  isperf2  20896  isperf3  20897  nrmsep3  21099  isconn2  21157  iskgen3  21292  ptpjpre1  21314  tx1cn  21352  tx2cn  21353  hausdiag  21388  qustgplem  21864  istdrg2  21921  isngp2  22341  isngp3  22342  isnvc2  22443  isclmp  22837  iscvs  22867  isncvsngp  22889  ovoliunlem1  23210  ismbl2  23235  i1f1lem  23396  i1fres  23412  itg1climres  23421  pilem1  24143  ellogrn  24244  ellogdm  24319  1cubr  24503  atandm  24537  atandm2  24538  atandm3  24539  atandm4  24540  atans2  24592  eldmgm  24682  isfusgrcl  26135  iscusgrvtx  26238  iscusgredg  26240  isph  27565  h2hcau  27724  h2hlm  27725  issh2  27954  isch2  27968  h1dei  28297  elbdop2  28618  dfadj2  28632  cnvadj  28639  hhcno  28651  hhcnf  28652  eleigvec2  28705  riesz2  28813  rnbra  28854  elat2  29087  ofpreima  29349  mpt2mptxf  29361  f1od2  29383  maprnin  29390  xrofsup  29418  xrdifh  29427  cmpcref  29741  ofcfval  29983  ispisys2  30039  1stmbfm  30145  2ndmbfm  30146  eulerpartlems  30245  eulerpartlemgc  30247  eulerpartlemv  30249  eulerpartlemd  30251  eulerpartlemr  30259  eulerpartlemn  30266  ballotlemodife  30382  sgn3da  30426  bnj945  30605  bnj1172  30830  bnj1296  30850  snmlval  31074  dfres3  31410  eldm3  31413  brtxp2  31683  brpprod3a  31688  dffun10  31716  elfuns  31717  brimg  31739  dfrdg4  31753  ellines  31954  opnrebl  32010  bj-ax12ig  32310  bj-equsexval  32333  bj-cleljustab  32545  bj-csbsnlem  32598  bj-mpt2mptALT  32748  bj-elid3  32759  bj-eldiag  32763  taupilem3  32837  topdifinffinlem  32866  relowlssretop  32882  istotbnd3  33241  isbnd2  33253  isbnd3b  33255  exidcl  33346  isdrngo2  33428  isdrngo3  33429  iscrngo2  33467  isdmn2  33525  isfldidl2  33539  isdmn3  33544  islshpat  33823  iscvlat2N  34130  ishlat3N  34160  snatpsubN  34555  diclspsn  36002  isnacs2  36788  islnm2  37167  islnr2  37204  islnr3  37205  issdrg2  37288  isdomn3  37302  elinintab  37401  elmapintab  37422  elinlem  37424  cnvcnvintabd  37426  k0004lem1  37966  dffo3f  38873  2reu8  40526  dfdfat2  40545  isodd2  40877  iseven5  40905  isodd7  40906  oddprmne2  40953  ismhm0  41123  sgrp2sgrp  41182  0ringdif  41188  isrnghmmul  41211  eliunxp2  41430  mpt2mptx2  41431  elbigo  41667
  Copyright terms: Public domain W3C validator