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  3647  elrab3  3678  dfpss3  4060  rabsn  4649  elrint2  4909  opres  5856  cores  6095  elpredg  6155  fnres  6467  fvres  6682  fvmpti  6760  f1ompt  6867  fliftfun  7054  isocnv3  7074  riotaxfrd  7137  ovid  7280  nlimon  7555  limom  7584  brdifun  8307  xpcomco  8595  0sdomg  8634  f1finf1o  8733  ordtypelem9  8978  isacn  9458  alephinit  9509  isfin5-2  9801  pwfseqlem1  10068  pwfseqlem3  10070  pwfseqlem4  10072  ltresr  10550  xrlenlt  10694  znnnlt1  11997  difrp  12415  elfz  12886  fzolb2  13033  elfzo3  13042  fzouzsplit  13060  rabssnn0fi  13342  caubnd  14706  ello12  14861  elo12  14872  bitsval2  15762  smueqlem  15827  rpexp  16052  ramcl  16353  ismon2  16992  isepi2  16999  isfull2  17169  isfth2  17173  isghm3  18297  gastacos  18378  sylow2alem2  18672  lssnle  18729  isabl2  18844  submcmn2  18888  iscyggen2  18929  iscyg3  18934  cyggexb  18948  gsum2d2  19023  dprdw  19061  dprd2da  19093  iscrng2  19242  dvdsr2  19326  dfrhm2  19398  sdrgacs  19509  islmhm3  19729  isdomn2  20000  psrbaglefi  20080  mplsubrglem  20147  prmirredlem  20568  chrnzr  20605  iunocv  20753  iscss2  20758  ishil2  20791  obselocv  20800  bastop1  21529  isclo  21623  maxlp  21683  isperf2  21688  restperf  21720  cnpnei  21800  cnntr  21811  cnprest  21825  cnprest2  21826  lmres  21836  iscnrm2  21874  ist0-2  21880  ist1-2  21883  ishaus2  21887  tgcmp  21937  cmpfi  21944  dfconn2  21955  t1connperf  21972  subislly  22017  tx1cn  22145  tx2cn  22146  xkopt  22191  xkoinjcn  22223  ist0-4  22265  trfil2  22423  fin1aufil  22468  flimtopon  22506  elflim  22507  fclstopon  22548  isfcls2  22549  alexsubALTlem4  22586  ptcmplem3  22590  tgphaus  22652  xmetec  22971  prdsbl  23028  blval2  23099  isnvc2  23235  isnghm2  23260  isnmhm2  23288  0nmhm  23291  xrtgioo  23341  cncfcnvcn  23456  evth  23490  nmhmcn  23651  cmsss  23881  lssbn  23882  srabn  23890  ishl2  23900  ivthlem2  23980  0plef  24200  itg2monolem1  24278  itg2cnlem1  24289  itg2cnlem2  24290  ellimc2  24402  dvne0  24535  ellogdm  25149  dcubic  25351  atans2  25436  amgm  25495  ftalem3  25579  pclogsum  25718  dchrelbas3  25741  lgsabs1  25839  dchrvmaeq0  26007  rpvmasum2  26015  tgjustf  26186  clwwlkwwlksb  27760  ajval  28565  bnsscmcl  28572  axhcompl-zf  28702  seq1hcau  28891  hlim2  28896  issh3  28923  lnopcnre  29743  dmdbr2  30007  elatcv0  30045  iunsnima  30297  ecxpid  30852  1stmbfm  31417  2ndmbfm  31418  eulerpartlemd  31523  oddprm2  31825  lfuhgr  32261  cvmlift2lem12  32458  bj-rest10  34273  topdifinfeq  34513  finxpsuclem  34560  curunc  34755  istotbnd2  34929  sstotbnd2  34933  isbnd3b  34944  totbndbnd  34948  ecres2  35417  islnr2  39592  areaquad  39701  afv2res  43315  oddm1evenALTV  43717  oddp1evenALTV  43718
  Copyright terms: Public domain W3C validator