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

Theorem syl6ibr 227
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 10-Jan-1993.)
Hypotheses
Ref Expression
syl6ibr.1
syl6ibr.2
Assertion
Ref Expression
syl6ibr

Proof of Theorem syl6ibr
StepHypRef Expression
1 syl6ibr.1 . 2
2 syl6ibr.2 . . 3
32biimpri 206 . 2
41, 3syl6 33 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  3imtr4g  270  imp4a  589  nic-ax  1506  nfimd  1917  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  euim  2344  mopick2  2362  2moswap  2369  2eu1OLD  2377  2eu6  2383  necon3adOLD  2668  necon3d  2681  necon1d  2682  ralrimd  2861  spcimegf  3188  spcegf  3190  spcimedv  3193  spc2gv  3197  spc3gv  3199  rspcimedv  3212  eqsbc3r  3389  ra4vOLD  3424  ra4OLD  3426  tpid3g  4145  pwpw0  4178  sssn  4188  pwsnALT  4244  ssiun  4372  ssiun2  4373  reusv6OLD  4663  wefrc  4878  tron  4906  ordtri3or  4915  oneqmini  4934  dmcosseq  5269  relssres  5316  restidsing  5335  trin2  5395  ssrnres  5450  sossfld  5459  fnun  5692  f1oun  5840  brprcneu  5864  ssimaex  5938  chfnrn  5998  dffo4  6047  dffo5  6048  fvclss  6154  isomin  6233  isofrlem  6236  isoselem  6237  fnoprabg  6403  nnsuc  6717  f1oweALT  6784  bropopvvv  6880  frxp  6910  poxp  6912  fnse  6917  mpt2xopynvov0g  6961  issmo2  7039  smores  7042  smogt  7057  rdglim2  7117  tz7.48lem  7125  tz7.49  7129  swoer  7358  qsss  7391  domtriord  7683  pssnn  7758  ssfi  7760  findcard  7779  findcard2  7780  findcard3  7783  frfi  7785  dffi3  7911  supmo  7932  inf3lem4  8069  carddom2  8379  fidomtri2  8396  pm54.43  8402  infpwfien  8464  alephordi  8476  cardaleph  8491  carduniima  8498  cardinfima  8499  alephval3  8512  dfac5lem4  8528  dfac5  8530  dfac2  8532  kmlem2  8552  cflm  8651  cfslb2n  8669  cfsmolem  8671  isf32lem9  8762  axcc4  8840  domtriomlem  8843  zorn2lem4  8900  zorn2lem6  8902  fpwwe2lem11  9039  fpwwe2lem12  9040  inttsk  9173  inar1  9174  intgru  9213  ingru  9214  indpi  9306  nqpr  9413  ltaddpr  9433  ltexprlem1  9435  ltexprlem5  9439  reclem2pr  9447  reclem4pr  9449  zmulcl  10937  uzm1  11140  uzwo  11173  uzwoOLD  11174  negn0  11197  xmullem2  11486  icoshft  11671  difreicc  11681  fzouzsplit  11860  ssfzoulel  11906  seqf1olem1  12146  seqf1olem2  12147  hashtpg  12523  swrdnd  12657  swrdccatin2  12712  modfsummod  13608  incexclem  13648  sqrt2irr  13982  dvds2lem  13996  dvdslelem  14030  divalglem8  14058  euclemma  14249  iserodd  14359  ramcl  14547  mreiincl  14993  joinfval  15631  meetfval  15645  dirge  15867  sylow2alem1  16637  efgredlemb  16764  kerf1hrm  17392  lbspss  17728  lspsneu  17769  lspsnat  17791  lspsncv0  17792  opsrtoslem2  18149  distop  19497  epttop  19510  isclo2  19589  restdis  19679  subbascn  19755  cnrest2  19787  cnpresti  19789  isnrm2  19859  cmpsublem  19899  cmpcld  19902  dfcon2  19920  t1conperf  19937  1stcrest  19954  lly1stc  19997  uptx  20126  txcn  20127  prdstopn  20129  txcon  20190  cmphaushmeo  20301  fbasrn  20385  csdfil  20395  trufil  20411  fclscf  20526  alexsubALTlem3  20549  alexsubALT  20551  haustsms2  20635  ovoliunlem1  21913  ovoliunnul  21918  volsup2  22014  coeaddlem  22646  plymul0or  22677  radcnv0  22811  wilthlem3  23344  chtub  23487  2sqlem10  23649  pntpbnd1  23771  mptelee  24198  axeuclidlem  24265  axcontlem4  24270  usgrarnedg  24384  usgraedg4  24387  frgrancvvdeqlemA  25037  frgrancvvdeqlemC  25039  isch3  26159  shmodsi  26307  orthin  26364  h1datomi  26499  stcltr2i  27194  atom1d  27272  sumdmdii  27334  cdj3lem1  27353  disjpreima  27445  lmxrge0  27934  dmvlsiga  28129  sibfof  28282  erdszelem9  28643  cvmlift2lem1  28747  fundmpss  29196  tfisg  29284  wfisg  29289  frinsg  29325  poseq  29333  sltval2  29416  nodenselem7  29447  nofulllem5  29466  outsideofrflx  29777  mblfinlem3  30053  itg2addnclem3  30068  nn0prpwlem  30140  ivthALT  30153  fnessref  30175  neibastop2lem  30178  tailfb  30195  cover2  30204  fdc  30238  nninfnub  30244  equivtotbnd  30274  prdstotbnd  30290  cntotbnd  30292  ablo4pnp  30342  isdrngo3  30362  crngohomfo  30403  intidl  30426  or32dd  30494  prtlem90  30598  prtlem18  30618  prter2  30622  nzss  31222  2reu1  32191  lswn0  32343  usgedgimp  32403  usgedgimpALT  32406  tpres  32554  2zrngamgm  32745  3impexpbicom  33221  alrim3con13v  33304  tratrb  33307  onfrALTlem3  33316  onfrALTlem2  33318  onfrALTlem1  33320  trsspwALT2  33617  trsspwALT3  33618  bnj600  33977  bnj1018  34020  bnj1173  34058  bnj1174  34059  bj-axtd  34182  bj-nfdt0  34248  bj-2upleq  34570  lsat0cv  34758  lfl1  34795  lkreqN  34895  atlrelat1  35046  pmaple  35485  pmapsub  35492  pclclN  35615  pclfinN  35624  osumcllem4N  35683  pexmidlem1N  35694  cdleme7ga  35973  lcfl7N  37228
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