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 666
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 665 . 2 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ↔ (𝜑𝜒)))
31, 2mpbi 218 1 ((𝜑𝜓) ↔ (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382
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 195  df-an 384
This theorem is referenced by:  pm5.32ri  667  biadan2  671  anbi2i  725  abai  831  anabs5  846  pm5.33  917  cases  1003  equsexvw  1918  equsexv  2094  equsexALT  2281  2sb5rf  2438  2eu8  2547  eq2tri  2670  rexbiia  3021  reubiia  3103  rmobiia  3108  rabbiia  3160  ceqsrexbv  3306  euxfr  3358  2reu5  3382  dfpss3  3654  eldifpr  4151  eldiftp  4174  eldifsn  4259  elrint  4447  elriin  4523  reuxfrd  4814  opeqsn  4886  rabxp  5068  copsex2gb  5142  eliunxp  5169  restidsing  5364  ressn  5574  dflim2  5684  fncnv  5862  dff1o5  6044  respreima  6237  dff4  6266  dffo3  6267  f1ompt  6275  fsn  6293  fconst3  6360  fconst4  6361  eufnfv  6373  dff13  6394  f1mpt  6397  isocnv3  6460  isores2  6461  isoini  6466  eloprabga  6623  mpt2mptx  6627  resoprab  6632  elrnmpt2res  6650  ov6g  6674  dfwe2  6850  dflim3  6916  dflim4  6917  dfopab2  7090  dfoprab3s  7091  dfoprab3  7092  fparlem1  7141  fparlem2  7142  brtpos2  7222  dftpos3  7234  tpostpos  7236  dfsmo2  7308  dfrecs3  7333  tz7.48-1  7402  ondif1  7445  ondif2  7446  elixp2  7775  mapsnen  7897  xpcomco  7912  eqinf  8250  infempty  8272  r0weon  8695  isinfcard  8775  dfac5lem1  8806  fpwwe  9324  axgroth6  9506  axgroth3  9509  elni2  9555  indpi  9585  recmulnq  9642  genpass  9687  lemul1a  10726  sup3  10829  elnn0z  11223  elznn0  11225  elznn  11226  eluz2b1  11591  eluz2b3  11594  elfz2nn0  12255  elfzo3  12310  shftidt2  13615  clim0  14031  fprod2dlem  14495  divalglem4  14903  ndvdsadd  14918  gcdaddmlem  15029  algfx  15077  isprm3  15180  isprm5  15203  isprm7  15204  xpsfrnel  15992  isacs2  16083  isfull2  16340  isfth2  16344  tosso  16805  odudlatb  16965  nsgacs  17399  isgim2  17476  isabl2  17970  iscyg3  18057  iscrng2  18332  isdrng2  18526  drngprop  18527  islmim2  18833  islpir2  19018  isnzr2  19030  iunocv  19786  ishil2  19824  islinds2  19913  ssntr  20614  isclo2  20644  isperf2  20708  isperf3  20709  nrmsep3  20911  iscon2  20969  iskgen3  21104  ptpjpre1  21126  tx1cn  21164  tx2cn  21165  hausdiag  21200  qustgplem  21676  istdrg2  21733  isngp2  22152  isngp3  22153  isnvc2  22246  isclmp  22636  iscvs  22664  isncvsngp  22683  ovoliunlem1  22994  ismbl2  23019  i1f1lem  23179  i1fres  23195  itg1climres  23204  pilem1  23926  ellogrn  24027  ellogdm  24102  1cubr  24286  atandm  24320  atandm2  24321  atandm3  24322  atandm4  24323  atans2  24375  eldmgm  24465  isph  26867  h2hcau  27026  h2hlm  27027  issh2  27256  isch2  27270  h1dei  27599  elbdop2  27920  dfadj2  27934  cnvadj  27941  hhcno  27953  hhcnf  27954  eleigvec2  28007  riesz2  28115  rnbra  28156  elat2  28389  ofpreima  28654  mpt2mptxf  28666  f1od2  28693  maprnin  28700  xrofsup  28729  xrdifh  28738  cmpcref  29051  ofcfval  29293  ispisys2  29349  1stmbfm  29455  2ndmbfm  29456  eulerpartlems  29555  eulerpartlemgc  29557  eulerpartlemv  29559  eulerpartlemd  29561  eulerpartlemr  29569  eulerpartlemn  29576  ballotlemodife  29692  sgn3da  29736  bnj945  29904  bnj1172  30129  bnj1296  30149  snmlval  30373  dfres3  30708  eldm3  30711  nofulllem5  30911  brtxp2  30964  brpprod3a  30969  dffun10  30997  elfuns  30998  brimg  31020  dfrdg4  31034  ellines  31235  opnrebl  31291  bj-ax12ig  31608  bj-equsexval  31633  bj-csbsnlem  31886  bj-mpt2mptALT  32049  bj-elid3  32060  bj-eldiag  32064  taupilem3  32138  topdifinffinlem  32167  relowlssretop  32183  istotbnd3  32536  isbnd2  32548  isbnd3b  32550  exidcl  32641  isdrngo2  32723  isdrngo3  32724  iscrngo2  32762  isdmn2  32820  isfldidl2  32834  isdmn3  32839  islshpat  33118  iscvlat2N  33425  ishlat3N  33455  snatpsubN  33850  diclspsn  35297  isnacs2  36083  islnm2  36462  islnr2  36499  islnr3  36500  issdrg2  36583  isdomn3  36597  elinintab  36696  elmapintab  36717  elinlem  36719  cnvcnvintabd  36721  k0004lem1  37261  dffo3f  38155  2reu8  39638  dfdfat2  39658  isodd2  39884  iseven5  39912  isodd7  39913  oddprmne2  39960  isfusgrcl  40535  iscusgrvtx  40638  iscusgredg  40640  ismhm0  41590  sgrp2sgrp  41649  0ringdif  41655  isrnghmmul  41678  eliunxp2  41900  mpt2mptx2  41901  elbigo  42138
  Copyright terms: Public domain W3C validator