MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6ib Unicode version

Theorem syl6ib 226
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.)
Hypotheses
Ref Expression
syl6ib.1
syl6ib.2
Assertion
Ref Expression
syl6ib

Proof of Theorem syl6ib
StepHypRef Expression
1 syl6ib.1 . 2
2 syl6ib.2 . . 3
32biimpi 194 . 2
41, 3syl6 33 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  3imtr3g  269  exp4a  606  mtord  660  19.23v  1760  exlimd  1914  cbvexd  2026  axc9lem2  2040  equveliOLD  2089  axc14  2113  mo3  2323  2eu3  2379  2eu6  2383  exists2  2389  necon2bd  2672  necon1bdOLD  2676  necon4adOLD  2678  necon2d  2683  necon4d  2684  spcimgft  3185  eqsbc3r  3389  reupick  3781  prneimg  4211  invdisj  4441  trin  4555  pwssun  4791  wefrc  4878  ordtri3  4919  suc11  4986  eqbrrdva  5177  elreldm  5232  elres  5314  xp11  5447  ssrnres  5450  opelf  5752  dffo4  6047  onmindif2  6647  dftpos3  6992  swoer  7358  mapsn  7480  domtriord  7683  nneneq  7720  unblem1  7792  supnub  7942  en3lplem2  8053  suc11reg  8057  inf3lem2  8067  trcl  8180  tz9.13  8230  acndom  8453  carduniima  8498  cardinfima  8499  dfac5lem5  8529  fin23lem26  8726  hsmexlem2  8828  axcc4  8840  axdc3lem2  8852  axdclem2  8921  entric  8953  alephval2  8968  cfpwsdom  8980  fpwwe2lem9  9037  ltapr  9444  supsrlem  9509  sup2  10524  nnunb  10816  nneo  10971  indstr  11179  ngtmnft  11397  qsqueeze  11429  qextlt  11431  qextle  11432  icoshft  11671  injresinj  11926  rexuzre  13185  rexico  13186  summo  13539  rpnnen2  13959  divalglem5  14055  ndvdssub  14065  pc2dvds  14402  infpn2  14431  vdwnnlem3  14515  mreiincl  14993  intopsn  15882  pmtrrn2  16485  psgnunilem4  16522  ablfac1eulem  17123  lbsextlem3  17806  xrsdsreclb  18465  znleval  18593  elcls3  19584  isclo2  19589  tgcn  19753  cnprest  19790  ordthaus  19885  hauscmplem  19906  comppfsc  20033  kgencn2  20058  prdstopn  20129  xkohaus  20154  qtoptop2  20200  tgqtop  20213  filufint  20421  fclsbas  20522  alexsubALTlem3  20549  alexsubALTlem4  20550  ptcmplem2  20553  cldsubg  20609  isucn2  20782  metequiv2  21013  bcthlem5  21767  vieta1  22708  aannenlem2  22725  ulmbdd  22793  angpined  23161  rlimcnp2  23296  amgm  23320  ftalem3  23348  bposlem6  23564  cusgrares  24472  frgraun  24996  usgreg2spot  25067  rngosn3  25428  lnon0  25713  ocnel  26216  h1dn0  26470  cnlnssadj  26999  cvnbtwn2  27206  cvnbtwn3  27207  cvnbtwn4  27208  dmdbr2  27222  dmdbr3  27224  dmdbr4  27225  superpos  27273  atcvati  27305  mdsymlem4  27325  sumdmdii  27334  cdj3lem1  27353  mul2lt0bi  27569  elicoelioo  27589  archiabl  27742  erdszelem9  28643  untangtr  29086  3orel2  29088  dfon2lem6  29220  dfon2lem7  29221  nofv  29417  sltres  29424  nodenselem4  29444  nodenselem7  29447  outsideofrflx  29777  wl-mo3t  30021  mblfinlem2  30052  trer  30134  elicc3  30135  nn0prpw  30141  sdclem1  30236  fdc  30238  incsequz  30241  0rngo  30424  dmncan1  30473  bicomdd  30583  prtlem90  30598  prtlem15  30616  rngunsnply  31122  isprm7  31192  stoweidlem62  31844  atbiffatnnb  32108  2reu3  32193  copisnmnd  32497  ssralv2  33301  truniALT  33312  onfrALTlem3  33316  onfrALTlem2  33318  onfrALTlem1  33320  ax6e2ndeq  33332  bnj1280  34076  bj-cbvexdv  34301  lsatcvat  34775  lfl1  34795  hlrelat2  35127  cvrat  35146  linepsubN  35476  2llnma3r  35512  dihjatcclem4  37148  dochexmidlem1  37187
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 185
  Copyright terms: Public domain W3C validator