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

Theorem baib 536
Description: Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
Hypothesis
Ref Expression
baib.1 (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
baib (𝜓 → (𝜑𝜒))

Proof of Theorem baib
StepHypRef Expression
1 ibar 529 . 2 (𝜓 → (𝜒 ↔ (𝜓𝜒)))
2 baib.1 . 2 (𝜑 ↔ (𝜓𝜒))
31, 2syl6rbbr 291 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:  baibr  537  ceqsrexbv  3654  elrab3  3685  dfpss3  4067  rabsn  4656  elrint2  4916  opres  5862  cores  6101  elpredg  6161  fnres  6473  fvres  6688  fvmpti  6766  f1ompt  6873  fliftfun  7059  isocnv3  7079  riotaxfrd  7142  ovid  7285  nlimon  7559  limom  7588  brdifun  8313  xpcomco  8601  0sdomg  8640  f1finf1o  8739  ordtypelem9  8984  isacn  9464  alephinit  9515  isfin5-2  9807  pwfseqlem1  10074  pwfseqlem3  10076  pwfseqlem4  10078  ltresr  10556  xrlenlt  10700  znnnlt1  12003  difrp  12422  elfz  12893  fzolb2  13040  elfzo3  13049  fzouzsplit  13067  rabssnn0fi  13349  caubnd  14713  ello12  14868  elo12  14879  bitsval2  15769  smueqlem  15834  rpexp  16059  ramcl  16360  ismon2  16999  isepi2  17006  isfull2  17176  isfth2  17180  isghm3  18304  gastacos  18385  sylow2alem2  18679  lssnle  18736  isabl2  18851  submcmn2  18895  iscyggen2  18936  iscyg3  18941  cyggexb  18955  gsum2d2  19030  dprdw  19068  dprd2da  19100  iscrng2  19249  dvdsr2  19333  dfrhm2  19405  sdrgacs  19516  islmhm3  19736  isdomn2  20007  psrbaglefi  20087  mplsubrglem  20154  prmirredlem  20575  chrnzr  20612  iunocv  20760  iscss2  20765  ishil2  20798  obselocv  20807  bastop1  21536  isclo  21630  maxlp  21690  isperf2  21695  restperf  21727  cnpnei  21807  cnntr  21818  cnprest  21832  cnprest2  21833  lmres  21843  iscnrm2  21881  ist0-2  21887  ist1-2  21890  ishaus2  21894  tgcmp  21944  cmpfi  21951  dfconn2  21962  t1connperf  21979  subislly  22024  tx1cn  22152  tx2cn  22153  xkopt  22198  xkoinjcn  22230  ist0-4  22272  trfil2  22430  fin1aufil  22475  flimtopon  22513  elflim  22514  fclstopon  22555  isfcls2  22556  alexsubALTlem4  22593  ptcmplem3  22597  tgphaus  22659  xmetec  22978  prdsbl  23035  blval2  23106  isnvc2  23242  isnghm2  23267  isnmhm2  23295  0nmhm  23298  xrtgioo  23348  cncfcnvcn  23463  evth  23497  nmhmcn  23658  cmsss  23888  lssbn  23889  srabn  23897  ishl2  23907  ivthlem2  23987  0plef  24207  itg2monolem1  24285  itg2cnlem1  24296  itg2cnlem2  24297  ellimc2  24409  dvne0  24542  ellogdm  25154  dcubic  25356  atans2  25441  amgm  25501  ftalem3  25585  pclogsum  25724  dchrelbas3  25747  lgsabs1  25845  dchrvmaeq0  26013  rpvmasum2  26021  tgjustf  26192  clwwlkwwlksb  27766  ajval  28571  bnsscmcl  28578  axhcompl-zf  28708  seq1hcau  28897  hlim2  28902  issh3  28929  lnopcnre  29749  dmdbr2  30013  elatcv0  30051  iunsnima  30303  ecxpid  30858  1stmbfm  31423  2ndmbfm  31424  eulerpartlemd  31529  oddprm2  31831  lfuhgr  32267  cvmlift2lem12  32464  bj-rest10  34279  topdifinfeq  34519  finxpsuclem  34566  curunc  34760  istotbnd2  34935  sstotbnd2  34939  isbnd3b  34950  totbndbnd  34954  ecres2  35423  islnr2  39598  areaquad  39707  afv2res  43323  oddm1evenALTV  43691  oddp1evenALTV  43692
  Copyright terms: Public domain W3C validator